Re: [isabelle] make_string ; PolyML structure

And maybe related to the question below, what has happened to the PolyML structure? In an Isabelle session it seems to be reduced to a single
item, structure IntInf

(I would normally expect that PolyML.makestring would solve the problem I describe below)


On 19/06/18 14:06, Jeremy Dawson wrote:


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.