* Antiquotation @{make_string} inlines a function to print arbitrary
values similar to the ML toplevel. The result is compiler dependent
and may fall back on "?" in certain situations.
This is a reprise from the NEWS of Isabelle2009-2 (June 2010), but it is
now documented in the implementation manual as well (see e49bf0be79ba).
Unlike low-level PolyML.makestring, the @{make_string} antiquotation uses
the usual trickery for Isabelle vs. ML pretty printing, such that regular
Isabelle pretty trees should ultimately be shown in the result (e.g. the
Output dockable in Isabelle/jEdit).
There are further changes towards b7f908c99546, which refine ML toplevel
exception printing in round #42. If there are problems with anything
here, or anything else, I hope for descriptions and observations according
to sound standards of empirical science.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
