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