Email Gateway (Aug 19 2022 at 15:46): Email Gateway (Aug 19 2022 at 15:46):From: Lars Noschinski <noschinl@in.tum.de>
Hi,
consider the following code:
theory Scratch imports Pure begin
ML ‹
val x = 1
val y = yield_singleton Proof_Context.read_vars (@{binding x}, NONE,
NoSyn) @{context}
›
end
Then the output of the block is not attached to the ML command, but
rather to the "x" in the binding antiquotation.
Email Gateway (Aug 19 2022 at 15:47):From: Dmitriy Traytel <traytel@in.tum.de>
The same happens even with just
ML ‹ @{binding x} ›
Dmitriy
Email Gateway (Aug 19 2022 at 15:47):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 15:47):From: Lars Noschinski <noschinl@in.tum.de>
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
Email Gateway (Aug 19 2022 at 15:47):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 25 2024 at 04:18 UTC