[isabelle-dev] NEWS: ML antiquotation @{print}

[Lars Noschinski]

So what should I use before antiquotations are available? Should I still avoid PolyML.makestring?

Makarius <makarius at sketis.net> schrieb:

>* ML antiquotation @{print} inlines a function to print an arbitrary
>ML value, which is occasionally useful for diagnostic or demonstration
>purposes.
>
>
>This refers to Isabelle/386e4cb7ad68, which also points to the place where 
>the older antiquotation @{make_string} is documented.
>
>Despite these official Isabelle/ML tools for debugging and diagnostics, I 
>sometimes see low-level ML traditionalists who are stuck with PolyML.print 
>or PolyML.makestring -- but there are no reasons for that, apart from old 
>habits.  David Matthews has provided better entry points for that several 
>years ago, and the above antiquotations make use of them.
>
>
> 	Makarius
>_______________________________________________
>isabelle-dev mailing list
>isabelle-dev at in.tum.de
>https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev