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.


	Makarius




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