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.



From: cl-isabelle-users-bounces at [cl-isabelle-users-bounces at] on behalf of Jeremy Dawson [Jeremy.Dawson at]
Sent: Tuesday, 19 June 2018 6:06 AM
To: cl-isabelle-users at
Subject: [isabelle] make_string


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?



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