Re: [isabelle] Printing full ML output in Isabelle/jEdit

On 23/07/16 15:28, Victor Dumitrescu wrote:
> I am struggling with printing the full output of ML code in Isabelle/jEdit.
> Specifically, I cannot figure out how to print the full contents of a
> list (the default is 10). I have tried increasing PolyML.print_depth,
> with no effect.

See ML_print_depth as explained in the Isabelle/Isar implementation
manual. It is actually about Isabelle/ML. Maybe this should be made more
clear somewhere.

> Also, when using Thm.proof_body_of, for example, the output seems to be
> elided in many places (output in Isabelle/jEdit attached below). Is
> there a way to retrieve the full output of the function?

You get the full output as a value in ML. The text representation is
only an approximation in semi human-readable form.

If you want to do anything specific with the printed text, there are
usually operations with names like string_of_FOO or pretty_FOO. This
representation of the output can then be displayed via the functions
"writeln" or "Pretty.writeln".


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.