Re: [isabelle] make_string

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.