On Fri, 3 Oct 2014, Tjark Weber wrote:
Note that "use" and "print" have different status in the Basis Library, which explicitly states that "[i]mplementations are not required to supply a use function."
In the wild times before the rather strict SML standards, both "use" and "print" where commonly available -- something every LISP programmer would expect anyway. Note that it was actually
print: 'a -> unit
and not the boring
TextIO.print: 'a -> unit
that we have today.
David Matthews has cultivated quite nice non-standard facilities both for "use" (or "eval") and "print" / "makestring" / "pretty" for arbitrary values. All this is available in Isabelle/ML, but the SML IDE uses strict SML'97 and spoils this game.
Printing values in the notation of the compiler is a bit impolite for proper programs anyway. It is mainly for experimentation and debugging. Proper integration of the Poly/ML debugger into the IDE might circumvent this potential limitation, but it is more work that is still to do.
Right now it is possible to use SML_import to pick useful add-ons from the Isabelle/ML environment and use them in SML, as well. See also $ISABELLE_HOME/src/Tools/SML/Examples.thy
Makarius