Re: [isabelle] Isabelle2014-RC2 issues: Output markup for ML-blocks



On Thu, 7 Aug 2014, Lars Noschinski wrote:

I can't say on the spot if it would be better of not doing that for ML
toplevel output.  Note that @{make_string} uses the same mechanism and
the next incident might be a lack of a position where it is normally
expected. On the other hand, @{make_string} is just for one-shot
experimentation and debugging, and proper production code has to
compose error messages more carefully anyway, using Position.here or
Binding.print explicitly.

What was confusing to me was the lack of any output for the ML block (it is in the output window, but there are no gray lines under the "ML") -- the annotated @{binding x} was more a curiosity. So attaching the output also to the ML command (and not only to the mentioned positions) would remove the confusing part of this issue for me.

The general principle here: if a message mentions precise positions in its header or its body it is attached to the corresponding spots in the source text; if it lacks precise positions it is attached to the command keyword instead. (And if it even lacks a proper transaction id in the header, it is dumped on Raw Output.)

It seems that in the past 3 years there was rarely a situation to become aware of that, which might be a good sign.

I will accumulate further possible refinements on the TODO list for the time after the Isabelle2014 release.


	Makarius




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