[isabelle] Printing full ML output in Isabelle/jEdit



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?

PBody {oracles = [], proof =
                PThm (1062004,
(("Tree.invert_inv", Const ("HOL.Trueprop", "bool â prop") $ (Const ("...", "(tree â bool) â bool") $ ...), NONE),
                       PBody {oracles = [], proof = MinProof, thms =
[(1062003, ("", ... $ ..., PBody {oracles = [...], ...})), (284, ("...", ..., ...)), (280, ("...", ...))]})),
                thms = [(1062004,
                         ("Tree.invert_inv",
Const ("HOL.Trueprop", "bool â prop") $ (Const ("HOL.All", "(tree â bool) â bool") $ Abs ("p", "tree", ...)),
                          PBody {oracles = [], proof = MinProof, thms =
[(1062003, ("", Const ("...", "bool â prop") $ ..., PBody {oracles = [...], proof = ..., thms = [...]})), (284, ("Pure.protectD", ... $ ... $ ..., PBody {oracles = [...], ...})), (280, ("...", ..., ...))]}))]}


Thank you,
Victor Dumitrescu

--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.





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