[isabelle-dev] NEWS: Antiquotation @{make_string}

[Makarius]

* 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