Re: [isabelle] Feature request: definition on crtl+hover



On Tue, 18 Dec 2012, Holger Blasum wrote:

You're right what is interesting is the definition as defined by the user, not the one internally seen by Isabelle (iirc debuggers also do it this way). Does Isabelle internally only keep track of where the definition begins (theory file, offset within the theory file) or also where it ends? (The latter would allow cutting the text ...)

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.


Further inspection revealed that inserting "Style jEdit* SloppyFocus" also fixes the disappearing jEdit subwindow for my configuration (without having to use SloppyFocus elsewhere).

I will look at this again myself. Someone else has reported focus inversion problems with the latest Unity/Compiz of Ubuntu 12.10, so this might be more than just an incident of vintage window managers.


	Makarius





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