Re: [isabelle] Feature request: definition on crtl+hover
Dear Isabelle Users,
I have a simple question (request?) considering this topic of discussion.
I find this
feature extremely helpful, especially when after Ctrl+Hover+click
a definition/rule/lemma in any theory which happens to be part of Main.
For instance, in the last few days I have been a bit engaged in writing
proofs in Isar which are concerned with the splitting of if´s. So after
to HOL.thy and examining the split_if lemma I wanted to continue
using this (Ctrl+Hover+Click) feature and jumping to the definition of the
case_split rule, for
But this feature does not seem to available any more in the file HOL.thy or
theory loaded in jedit and which is part of Main. Am I doing
something wrong here [...probably...]?
On Thu, Jan 3, 2013 at 12:46 PM, Makarius <makarius at sketis.net> wrote:
> On Wed, 2 Jan 2013, Holger Blasum wrote:
> On 12-22, Makarius wrote:
>>> There is sufficient information to determine the full definition
>>> range, lets say the language element like "fun ..." with all its
>>> equations, or "function ..." with the following proof. For the
>>> latter example there is a special case, though: there is a second
>>> part following somewhere as "termination ..." which is not directly
>>> Anything else should work smoothly, one the reference to sources is
>>> wired up properly in the editor.
>> "Sufficient information to determine the full definition range"
>> sounds promising :-)
>> Why am I asking whether the end point information is available?
>> To my post of 17 Dec I attached a file hover.thy:
>> If we know that the definition of "mysucc" is in file hover.thy,
>> characters 0x49 to 0x5a, then it could perhaps be easy to implement
>> to display this information (that is, in this example, "mysucc n = n + 1")
>> once you ctrl+hover on mysucc (without having to jump through
>> the theories). From a usage perspective, I think
>> this could be very convenient, especially if one reads a theory
>> sb else has written ("what was this abbreviation she is using ...").
> The "definition range" is the whole command span, starting with
> "definition ..." and ending with "mysucc n = n + 1" in this example. This
> is what I meant to show in the popup eventually.
> In general, there is not just one equation defining a term, e.g. in "fun"
> with several recursive equations, or several functions defined at the same
> time. Showing the whole specification text should give sufficient clues to
> the user. Lets see again how it looks when it is actually there (not in
> the coming release.)
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil
This archive was generated by a fusion of
Pipermail (Mailman edition) and