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
shortcut Ctrl-`.

I did not know this one yet -- Fabian is lucky with his US keyboard layout.

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


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.


	Makarius





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