Email Gateway (Aug 21 2021 at 16:00): Email Gateway (Aug 21 2021 at 16:00):From: Walther Neuper <walther.neuper@jku.at>
it's helpful to watch people fluent in Isabelle/jEdit, for instance, how
they use "semantic selection" when polishing code.
In the days of video conferencing one has to lookup "semantic selection"
in the Isabelle/jEdit manual, and that might be hard.
The respective explanation on p.31 is "/A mouse click with C modifier,
or the action isabelle.goto-entity (shortcut CS+d) jumps to the original
defining position/."
I use <Strg>+<left-mouse> and this works fine. And then I read:
"/The action isabelle.select-entity (shortcut CS+ENTER) supports
seman//tic selection of all occurrences of the formal entity at the
caret position, with a defining position in the current editor buffer./"
But which keys / mouse-actions are /CS+ENTER/ on a standard keyboard
under Linux?
Walther
Email Gateway (Aug 21 2021 at 16:13):From: Dominique Unruh <unruh@ut.ee>
Hello,
CS+Enter is short for Ctrl-Shift-Enter. So on you keyboard, which
apparently has German labels, it would be Strg-Shift-Enter. (And the
goto-entity would be Strg-Shift-C.)
Best wishes,
Dominique.
Email Gateway (Aug 21 2021 at 18:32):From: Walther Neuper <walther.neuper@jku.at>
On 21.08.21 18:13, Dominique Unruh wrote:
Hello,
CS+Enter is short for Ctrl-Shift-Enter. So on you keyboard, which
apparently has German labels, it would be Strg-Shift-Enter. (And the
goto-entity would be Strg-Shift-C.)great to get a response on this mailing list even during weekend.
And now I'm motivated to continue during weekend ;-) thank you!
I get the situation shown in Figure 3.8 of the manual with clicking one
instance of a particular identifier, well. And then I want to rename all
of them at once as shown in Figure 3.9.
There are lots of combinations for actions with <Ctrl-Shift-Enter> +
editing ?+mouse? and I tried a lot of them; so far I cannot state success.
The listeners in this list will find this statement amusing; showing the
solution takes a second, but explaining it in words would take much longer.
I'll continue, even if I get a verbal explanation only after the weekend ;-)
Best wishes,
Dominique.Best, Walther
On 8/21/21 6:59 PM, Walther Neuper wrote:
it's helpful to watch people fluent in Isabelle/jEdit, for instance,
how they use "semantic selection" when polishing code.In the days of video conferencing one has to lookup "semantic
selection" in the Isabelle/jEdit manual, and that might be hard.The respective explanation on p.31 is "/A mouse click with C
modifier, or the action isabelle.goto-entity (shortcut CS+d) jumps to
the original defining position/."I use <Strg>+<left-mouse> and this works fine. And then I read:
"/The action isabelle.select-entity (shortcut CS+ENTER) supports
seman//tic selection of all occurrences of the formal entity at the
caret position, with a defining position in the current editor buffer./"But which keys / mouse-actions are /CS+ENTER/ on a standard keyboard
under Linux?Walther
Email Gateway (Aug 22 2021 at 21:23):From: Makarius <makarius@sketis.net>
After the action isabelle.select-entity you are in multi-selection mode as
described in the Original jEdit Documentation (jedit-manual, section "Multiple
Selection").
In particular the text says:
"""
Commands that insert (or paste) text replace each selection with the entire
text that is being inserted.
"""
In other words: you mere continue typing, and the result will show up in all
places. (If something goes wrong, it is a bit awkward to repair: I usually do
plain undo and start again.)
Makarius
Last updated: Jan 04 2025 at 20:18 UTC