Re: [isabelle] make_string



Hi Makarius,

Thanks for the information that I shouldn't be using @{make_string}.
This raises the obvious question of what I should be using. Would it be possible for you to tell me that? Ie, what is the equivalent in the
managed ML environment called "Isabelle/ML" of the PolyML function
PolyML.makestring?

Thanks

Jeremy

On 06/19/2018 07:30 PM, Makarius wrote:
On 19/06/18 06: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,

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?

See also section 0.2.4 Printing ML values in the "implementation"
manual, which is the first place to look for anything regarding
Isabelle/ML tool development.

In particular it says:

   This is occasionally useful for diagnostic or demonstration purposes.
   Note that production-quality tools require proper user-level error
   messages, avoiding raw ML values in the output.

In other words, you use @{make_string} or more conveniently @{print} for
temporary output experiments, but use regular user-space print
operations for real output. The latter depends on what types of values
you want to print, and what is the purpose of it.


	Makarius





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