Re: [isabelle] Feature request: definition on crtl+hover
On Mon, 17 Dec 2012, Fabian Immler wrote:
There is also jEdits command "Go to recent buffer" with its predefined
I did not know this one yet -- Fabian is lucky with his US keyboard
Myself I do it in a more basic way: C-W to close the target buffer. This
works under the assumption that it is from the "library", i.e. you don't
care having it open or not.
2012/12/17 Lars Noschinski <noschinl at in.tum.de>:
You could try playing around with the Navigator extension.
I've found it unconvincing when I tried some months ago -- one of the
weaker jEdit plugins. It looks like really good navigation needs to be
provided as Isabelle/jEdit functionality. Don't hold your breath for the
coming release, though. If someone can point to a good specification how
this should work, lets say in Firefox, it can be accelerated. Or someone
else might sit down himself and improve the jEdit Navigator plugin
Another idea in the pipeline is to improve the content and flexibility of
the Isabelle/jEdit popup window: it could show you the part of the
relevant source outright, or some documentation. The next release will
already have a popup that is recursively again a jEdit text area at a
small scale, but without the extra functionality sketched here.
This archive was generated by a fusion of
Pipermail (Mailman edition) and