This is just a reminder of an important point that I am trying to make for
many months already:
PolyML.makestring has no practical purpose outside bootstrapping of
Isabelle/Pure. Most people can forget that it ever existed.
The @{make_string} antiquotation does a better job, with proper pretty
printing and formal markup. It is officially documented in the
"implementation" manual, including its inherent undefinedness of the
precise output.
Printing of internal ML values is for debugging, not for actual
application code, so it is better not committed at all. (Application code
with lots of optional debugging functionality routinely breaks down when
that is enabled.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
