Re: [isabelle] make_string



One more explanation to clarify why you see "<markup>" here.

@{make_string} produces a string containing special markup instructions
(e.g., for supporting ctrl-click in jEdit, type-annotations when hovering,
and many more things).
And now the ML toplevel gives you the value of the ML-value "str".
However, since ML-value are not necessarily strings, but complex values,
those values are pretty printed.
So, the ML-toplevel applies the equivalent to @{make_string} to the content
of "str".
And what you end up with is the result of the attempt to pretty print a
string with markup (namely, @{make_string} (@{make_string} something)).

If you use, e.g., "tracing" or "warning" to output the result of
@{make_string} instead, then you will get proper readable output.
(And "tracing (@{make_string} (@{make_string} something))" will output
"<markup>" no matter what 'something' is.)

Best wishes,
Dominique.




On 19 June 2018 at 12:30, Makarius <makarius at sketis.net> 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.