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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and