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

Makarius makarius at sketis.net
Mon Apr 8 17:46:01 CEST 2013

* 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.


More information about the isabelle-dev mailing list