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



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.


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