Re: [isabelle] Ctrl-Click on abbreviation from locale in image jumps to begin of context



On Wed, 4 Dec 2013, Andreas Lochbihler wrote:

I noticed that when I open a locale that has been defined in the image of the session and Ctrl-Click on an identifer which refers to an abbreviation in that locale, then Isabelle/jEdit jumps to the begin of the context block. I would have expected that it jumps to the declaration of the abbreviation as it does for definitions. Here's a MWE for Isabelle2013-1:

theory Scratch imports Main begin
(*1*)context partial_function_definitions begin
term "fixp_fun"
end
end

Ctrl-Click on fixp_fun jumps to (*1*), but I would prefer line 130 of Partial_Function.thy.

This is a general shortcoming due to the way how formal entities and their positions are managed internally. I have been aware of it when I introduced the concept some years ago, even before a usable Prover IDE front-end was available. Similar inconveniences happen when declarations and attributed fact expressions are processed in various situations of local context.

Further refinement of this area needs to be postponed until more serious problems are solved.


You are mentioning Isabelle2013-1 above. Can you also give quick try to http://isabelle.in.tum.de/website-Isabelle2013-2-RC3/ ? There are at least 24h more time, before I consider making the final snapshot for Isabelle2013-2.

Isabelle2013-1 did not work out so well, due to too few people putting hard measures of testing on it. You are the expert on getting to the limits of what is possible and what not ...


	Makarius




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