Re: [isabelle] make_string



Hi Jeremy,

Dose this function trm_to_string [1] do the job?

fun trm_to_string (ctxt:Proof.context) (trm:term) =  Syntax.string_of_term ctxt trm
 |> YXML.parse_body
 |> XML.content_of : string;

davidg's comment here [2] might be useful as well.

[1] https://github.com/data61/PSL/blob/master/PGT/PGT.ML#L23
[2] https://stackoverflow.com/questions/26007442/how-do-i-convert-thm-conji-to-an-ascii-string-i-can-save-to-a-file

Regards,
Yutaka

________________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk] on behalf of Jeremy Dawson [Jeremy.Dawson at anu.edu.au]
Sent: Tuesday, 19 June 2018 6:06 AM
To: cl-isabelle-users at lists.cam.ac.uk
Subject: [isabelle] make_string

Hi,

I find that when I use @{make_string} to get a string from a value, it
produces something which is reported simply as

val str = "<markup>": string,

its length (String.size) is something enormous, and when exploded into
an enormous list of characters, seems to incorporate some sort of
pretty-printing information.

How do I get it simply as a string?  There is a function writeln which
will print it on the screen as a sensible string, but how do I get this
string as an ML value?

thanks

Jeremy






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