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



On 07.08.2014 13:44, Makarius wrote:
> On Thu, 7 Aug 2014, Dmitriy Traytel wrote:
>
>>>  Then the output of the block is not attached to the ML command, but
>>>  rather to the "x" in the binding antiquotation.
>> The same happens even with just
>>
>> ML ‹ @{binding x} ›
>
> This behaviour has been for a long time, going back at least to
> Isabelle2011-1 (October 2011), which was the first official release of
> the Prover IDE.  (It is interesting to run that today to sense the
> depth of time of PIDE development.)
>
> As a general principle, a PIDE message is attached to all source
> positions that are mentioned in its body.  The ML pretty printer for
> type binding includes its original position.  This was done as a
> normal default: when a position is available it is included in output.
>
> 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.

  -- Lars




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