Email Gateway (Aug 22 2022 at 13:50): Email Gateway (Aug 22 2022 at 13:50):From: Victor Dumitrescu <victor.dumitrescu@ed.ac.uk>
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.
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?
Thank you,
Victor Dumitrescu
Email Gateway (Aug 22 2022 at 13:51):From: Makarius <makarius@sketis.net>
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".
Makarius
Email Gateway (Aug 22 2022 at 13:51):From: Lars Hupel <hupel@in.tum.de>
Hi Victor,
as far as I know, the canonical way of setting the print depth is via an
Isar attribute:
declare [[ML_print_depth=1000]]
Setting this to a sufficiently high value should also solve your problem
below. Beware that proof terms can be very big and pretty printing them
in full will produce a lot of output.
Cheers
Lars
Last updated: Nov 21 2024 at 12:39 UTC