Email Gateway (Aug 19 2022 at 15:02): Email Gateway (Aug 19 2022 at 15:02):From: Makarius <makarius@sketis.net>
jEdit is a surprisingly flexible editor. Apart from keyboard shortcuts,
it can map of any its "actions" to other GUI elements, e.g. the context
menu or tool bar.
I have recently kept an eye on this: providing actions for all important
entry points to the "Isabelle" plugin of jEdit. The Isabelle/jEdit manual
also covers that to some extent.
If anything important is not accessible via actions, just keep me
informed, especially so short before the release.
Makarius
Email Gateway (Aug 19 2022 at 15:02):From: Lars Noschinski <noschinl@in.tum.de>
I'd like to see an action for detaching the output window.
Email Gateway (Aug 19 2022 at 15:14):From: Christian Sternagel <c.sternagel@gmail.com>
Dear fellow users,
I'm now using some shortcuts for a while that might be of interest for
others. More specifically for the following actions (either via
Utilities -> Global Options ... -> jEdit -> Shortcuts; or by editing
$ISABELLE_HOME_USER/jedit/keymaps/imported_keymaps.props directly).
Output panel (Toggle): C+e o
in the props file: isabelle-output-toggle.shortcut=C+e o
Query panel (Toggle): C+e q
in the props file: isabelle-query-toggle.shortcut=C+e q
Sledgehammer panel (Toggle): C+e h (for hammering, since C+e s is
already given to select-fold by default)
in the props file: isabelle-sledgehammer-toggle.shortcut=C+e h
Theories panel (Toggle): C+e t
in the props file: isabelle-theories-toggle.shortcut=C+e t
A default shortcut that is useful together with those is "C+l" which
will scroll the buffer such that the cursor is centered vertically.
E.g., when your Query panel is at the bottom (as for me) and you are
working at the lower part of the buffer, after starting a query via C+e
q you will no longer see the caret position. Now C+l will scroll there
and give the focus back to the buffer. Thus you can conveniently edit
your thy file and at the same time read the query results.
cheers
chris
Last updated: Nov 21 2024 at 12:39 UTC