Email Gateway (Aug 19 2022 at 15:29): Email Gateway (Aug 19 2022 at 15:29):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Makarius,
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'm asking since while showing Isabelle/jEdit to others I often get the
question whether it wasn't possible to avoid using the mouse.
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?).
cheers
chris
Email Gateway (Aug 19 2022 at 15:30):From: Makarius <makarius@sketis.net>
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
http://worrydream.com/dbx/ helps again to revive the visions to work with
"modern" computer displays effectively.
Makarius
Email Gateway (Aug 19 2022 at 15:30):From: René Neumann <rene.neumann@in.tum.de>
Neither; it's increased productivity. When I'm typing with both hands,
but then need to transfer one hand to the mouse and spend several
seconds on aiming the pointer exactly where I need it, this is a larger
disruption. Especially when this switch has to be done quite often.
A mouse is an efficient tool, when I don't need the keyboard or resting
one hand there is sufficient, like for example for browsing, gaming or
others. But not for developing or writing in general.
It is also quite ok, when I'm only skimming through a theory and looking
at different things or try to understand a certain proof. Then it's ok
to point here and there.
mouse_ok <-> number_of_chars_to_write < 20
(or sth like that :))
Email Gateway (Aug 19 2022 at 15:31):From: Makarius <makarius@sketis.net>
I do use the mouse a lot in development, but maybe that's an instance of
gaming, or maybe I am just old-fashioned (being socialized when a mouse
was something very special).
If the reluctance to use the mouse is a general trend in "development"
then current IDEs must have keyboard shortcuts for the tooltip idioms that
we have. Maybe someone wants to look around and write a summary for the
situation in Eclipse, Netbeans, IntelliJ IDE, Visual Studio.
Makarius
Email Gateway (Aug 19 2022 at 15:31):From: Bertram Felgenhauer <bertram.felgenhauer@googlemail.com>
Christian Sternagel wrote:
I'd like to add to this, because I've been one of the people to bother
Chris with this question.
I'm not a strong opponent of using the mouse, though I think that having
keyboard shortcuts for common actions is very desirable for efficiency,
and looking up types of identifiers is a very common interaction when
using Isabelle, so deserves having such a shortcut. (Note that the
cursor will often be in the vicinity of the identifier of interest,
while the mouse pointer may be anywhere in the jedit window.)
Despite having no issues with using the mouse per se, I find C-hover
very annoying. There are two reasons for this with Isabelle/jedit's
default settings. The more important one is that my usual approach for
mouse interaction is to move the mouse to the right spot, and then click
appropriately. With C-hover, one has to press the Control key before the
mouse pointer comes to rest; if I forget doing that, I have to press
Control and wiggle with the mouse; rather than one interaction with the
mouse I now need two. The second issue I'm experiencing is that the
popup does not appear immediately, i.e. the UI forces me to wait.
Fortunately, one can reduce the popup delay to improve interactivity.
Cheers,
Bertram
Email Gateway (Aug 19 2022 at 15:31):From: bnord <bnord01@gmail.com>
In Eclipse there is F2 for the tool tip and F3 for open declaration and
of course a lot of other useful stuff, I virtually never use the mouse
when writing Scala code in Eclipse except for creating new run
configurations, during debugging and stuff, but even there I prefer
tabbing through forms and stuff over using the mouse.
Another feature I miss is instance highlighting to directly see where
the term/fact under the cursor is used and the equivalent of a call
hierarchy for theorems.
I don't use the other IDEs but I'm very confident that they'll have
similar features, a quick web search produced Crtl+F1 for InteliJ.
However I seldom use the tool tip in Isabelle/jEdit, what may be nice if
it wouldn't just show the type but also the definition and maybe a
selection of theorems in which the term appears, respectively the fact
itself when hovering a fact.
Keyboard support for open declaration together with for moving back and
forth would be nice. Yet this would become less necessary if the tool
tip already would show the definition, I use this a lot in my PDF viewer
(Skim, with the mouse) where hovering a link opens a tool tip showing
the linked position which is incredibly useful for looking up citations.
Best
Benedikt
Last updated: Apr 25 2024 at 16:19 UTC