Email Gateway (Aug 19 2022 at 11:49): Email Gateway (Aug 19 2022 at 11:49):From: Lars Hupel <hupel@in.tum.de>
(referring to Isabelle2013)
Consider the following snippet:
theory Foo
imports Main
begin
value x
As expected, nothing happens when Ctrl-clicking x, since it's a free
variable.
Now, change that to the following:
ML{*
@{term x}
*}
When you Ctrl-click x there, Isabelle/jEdit opens thm.ML, jumping to
the TFree constructor of datatype typ.
In contrast:
ML{*
@{term "x :: nat"}
*}
Ctrl-clicking x jumps to the Type constructor of datatype typ.
Email Gateway (Aug 19 2022 at 11:50):From: Makarius <makarius@sketis.net>
As a general principle, the Prover IDE (PIDE) markup allows the prover to
augment sources by aspects of its formal processing. Thus the front-end
basically visualizes a partial trace of what the prover did, when
digesting the text.
The prover consists of many languages and subsystems, so the markup might
consist of too much information (several competing languages) or too
little (languages that don't cope with PIDE markup yet).
In the examples above it is Isabelle/ML exposing markup produced by the
Poly/ML compiler that is invoked within a certain formal context and with
certain source positions. The ML antiquotation @{term} inlines a concrete
ML datatype value, so its markup tells about constructors of ML types
typ/term, as defined in src/Pure/term.ML.
That is neither a "bug" nor a "feature", not even strange. It is how PIDE
really works, in conjunction with other tools like the ML compiler.
You can see more about this as follows:
declare [[ML_trace]]
ML {* @{term "x :: nat"} *}
In some situations where the stack of markups on some text gets really
confusing, I have changed the implementation inside, to get its "trace" in
better presentable shape. (There have been funny situations where PIDE
markup has revealed odd tricks from the past to make the system do certain
things, but that is now revealed to the end-user and better avoided.)
Makarius
Email Gateway (Aug 19 2022 at 11:50):From: Lars Noschinski <noschinl@in.tum.de>
From this description, I would have expected it to jump to Free (the
outermost constructor) instead of TFree.
Without this description, I would have expected that nothing happens
when clicking on a free variable inside @{term}: For other atomic terms
(e.g. constants, free variables registered in the context), clicking
inside @{term} behaves like in other contexts, for example "lemma".
Also, the behaviour of @{term} differs from the behaviour of @{cterm},
for example.
So, for a user not thinking about the implementation of the system, this
feels definitely inconsistent.
-- Lars
Email Gateway (Aug 19 2022 at 11:50):From: Makarius <makarius@sketis.net>
On Mon, 23 Sep 2013, Lars Noschinski wrote:
Also, the behaviour of @{term} differs from the behaviour of @{cterm},
for example.
There is a very fundamental difference here: term is a concrete datatype
value that is inlined, and cterm is an abstract entity of the LCF kernel.
Users of Isabelle/ML need to get that understanding at some point.
So, for a user not thinking about the implementation of the system, this
feels definitely inconsistent.
Back to a general point: PIDE markup does many things, but not everything.
What it does was considered impossible some years ago, and users of other
proof assistants will be jaleous when they learn about it.
Further fine-tuning of the markup is one of these continous processes
(ongoing for 20-30 years) of making even better what is there already.
For markup produced by Poly/ML in particular, improvements come quicker
and more often when people manage to procure some funding for David
Matthews to do the work.
Makarius
Last updated: Apr 20 2024 at 12:26 UTC