Re: [isabelle] Isabelle2014-RC4: Isabelle/jEdit action for C-hover

On Wed, 20 Aug 2014, Christian Sternagel wrote:

Is there already an action (or command, I'm not sure on the naming here) in Isabelle/jEdit for whatever C-hover does internally. Then a keyboard shortcut could be assigned to it, avoiding the need to use the mouse.

I usually try to provide jEdit actions for the main things by default, but this is not always easy. For example, the "`" completion template is hard to reach on some national keyboards, so I tried to wrap it up as remappable action, but did not manage so far because of entangled GUI events.

Tooltips are also not so immediate. There are various GUI event listeners and timers around it. Ultimately it goes through PIDE.rendering().tooltip(). We've already seen smart approaches with Beanshell scripting on this mailing list, far beyond what I usually do myself, so maybe someone manages that.

I'm asking since while showing Isabelle/jEdit to others I often get the question whether it wasn't possible to avoid using the mouse.

I wonder where this anti-mouse movement is coming from. Nostalgic users of vi? Or bad mouse hardware? I am myself using a relatively old-fashioned 3-button-wheel mouse from 5 years ago, which might have been the peak of this technology. More recent touchpads also work for me, notably on Mac OS X.

Of course C-hover is possible recursively, which would not directly work with the keyboard currently (maybe if keyboard focus was transferred to the popup and there would be a cursor available?).

In principle the popup is a nested jEdit textarea, with special tricks around it to make it work smoothly. The cursor is disabled explicitly. After all this is not Emacs, with its "everything is a buffer approach".

Generally, I don't think that the single-focus text cursor is a good concept for the future. The Output panel also has that as retro-feature only. BTW, in the classic GUI terminology of Java/Swing, the "cursor" is actually the mouse pointer, and a text cursor within a text area is called "caret".

Maybe this talk from "1973" (actually 2013) by Bret Victor helps again to revive the visions to work with "modern" computer displays effectively.


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