Email Gateway (Aug 19 2022 at 13:17): Email Gateway (Aug 19 2022 at 13:17):From: Buday Gergely <gbuday@karolyrobert.hu>
Thanks it worked.
Working with
http://isabelle.in.tum.de/repos/isabelle/raw-file/79c92e2dc359/src/Doc/JEdit/JEdit.thy
I created a small patch so that the Isabelle/JEdit documentation would write about this feature:
--- JEdit.thy 2014-01-21 16:58:04.555705621 +0100
+++ JEdit-mod.thy 2014-01-21 17:02:50.450960114 +0100
@@ -480,9 +480,9 @@
\medskip A black rectangle in the text indicates a hyperlink that
may be followed by a mouse click (while the @{verbatim CONTROL} or
or @{verbatim COMMAND} and a backtick.
Also note that the link target may be a file that is itself not
subject to formal document processing of the editor session and thus
@@ -1138,4 +1138,4 @@
\end{itemize}
*}
Gergely
Email Gateway (Aug 19 2022 at 13:18):From: Lars Noschinski <noschinl@in.tum.de>
There is the "Navigator" plugin which can be installed over the plugin
manager. By default, it has no keybindings, though the can be configured
in Utilities / Global Options / jEdit / Shortcuts. Look for the "Back"
and "Forward" commands.
-- Lars
signature.asc
Email Gateway (Aug 19 2022 at 13:22):From: John Wickerson <johnwickerson@cantab.net>
Thanks Lars for suggesting the Navigator plugin. I found it very helpful for returning to my position after a CMD-click. Unfortunately I found today that Isabelle/jEdit wouldn't launch, it just gets stuck on the splash screen. It turns out that removing that plugin fixes the problem. I'm just putting this in writing in case anybody else finds the same problem.
John
Email Gateway (Aug 19 2022 at 13:22):From: Lars Noschinski <noschinl@in.tum.de>
I had this problem (jEdit getting stuck at the startup screen)
sporadically with (older) versions of jEdit. It always vanished on a
second try, so I never investigated it.
Email Gateway (Aug 19 2022 at 13:35):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi,
holding down ctrl and clicking on a name makes Isabelle/jedit to jump to the definition of that name.
However, the documentation says
Presently (Isabelle2013-2) there is no systematic navigation within the editor
to return to the original location.
Would implementing this be technically difficult or obviously there are more important things to do?
Email Gateway (Aug 19 2022 at 13:35):From: Lawrence Paulson <lp15@cam.ac.uk>
You mean, to go back to where you started from? Use ctrl- (CMD- on a Mac).
To allow navigation within a single document, use the Marks menu. It would be great if there were some sort of global bookmark system, but I don’t know of anything.
Larry
Email Gateway (Aug 19 2022 at 15:03):From: Makarius <makarius@sketis.net>
Isabelle2014-RC0 now has the Navigator plugin enabled. Please try it to
see if this important functionality works smoothly.
Makarius
Email Gateway (Aug 19 2022 at 15:03):From: Buday Gergely <gbuday@karolyrobert.hu>
Makarius wrote:
I installed it. If I have
theory Dummy
imports Main
begin
lemma "x Setprod y = 2"
ctrl-left-mouse-click on Setprod brings me to Group_Big.thy. The arrow in the menu then takes me back and forth, as in a browser, that is fine, thanks for the implementation.
However, when I try to ctrl-click on _finite_ in Group_Big.thy, the constant does not grow a border and Isabelle/JEdit does not jump to Finite_Set.thy. Is this the sought behaviour?
Email Gateway (Aug 19 2022 at 15:03):From: Makarius <makarius@sketis.net>
This is what the Isabelle/jEdit manual says:
Also note that the link target may be a file that is itself not subject
to formal document processing of the editor session and thus prevents
further exploration: the chain of hyperlinks may end in some source file
of the underlying logic image, or within the Isabelle/ML bootstrap
sources of Isabelle/Pure.
Makarius
Last updated: Apr 20 2024 at 12:26 UTC