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
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
