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
 transfers me
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
detailed
proofs in Isar which are concerned with the splitting of if´s. So after
jumping
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
example.

But this feature does not seem to available any more in the file HOL.thy or
any other
theory loaded in jedit and which is part of Main. Am I doing
something wrong here [...probably...]?

Best!

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
>>> connected.
>>>
>>> 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.)
>
>
>         Makarius
>
>
>


-- 
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 MHonArc.