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!

Jeremy

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.

[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.