Re: [isabelle] make_string

Hi Yutaka,

Thanks, that helps wonderfully.

Your function trm_to_string of course only works for terms, but
the following fixes the output of @{make_string}, exactly what I want

fun fix_markup str = str |> YXML.parse_body |> XML.content_of : string ;

Thanks again!


On 06/19/2018 07:05 PM, Nagashima, Yutaka wrote:
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.