Re: [isabelle] make_string

On 06/25/2018 07:33 PM, Makarius wrote:
On 25/06/18 11:02, Dominique Unruh wrote:

You will not get this from @{make_string}, only something similar
looking but unparseable.
@{make_string} gives you somewhat human readable output, for debugging
(which, in case of term is relatively raw, I assume that is because it
has to work on non-wellformed terms, too).
So - independent of whether it is production-suitable or it - it does
not seem to be what you are looking for.

This already summarizes the situation nicely: @{make_string} / @{print}
is for tracing and debugging while doing Isabelle/ML development. The
output is sometimes close to ML notation (e.g. term structure),
sometimes close to regular output (e.g. typ). In some situations there
might be no usable output at all: the exact side-conditions change over
time as the Poly/ML compiler evolves.

Thus it is suitable (and very useful) for adhoc tests, but not suitable
for another program reading the results. Even with perfect output, the
build-in print_depth prevents this. (The print_depth is very important
to avoid bombing the system when printing really big values.)

The default pretty printing with markup conforms to this overall idea of
@{make_string} / @{print} as adhoc diagnostic output. That was the start
of the thread: the <markup> that appears routinely when printing
structured values.


Hi Makarius,

From the length of this email thread, and the absence in it of any information giving an answer as to how I should be doing the equivalent of PolyML.makestring, I infer that this function has been made unavailable with nothing to take its place.

Is this so?  And if so, I'm curious as to why it was removed?



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