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



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.


	Makarius


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