Email Gateway (Aug 22 2022 at 14:31): Email Gateway (Aug 22 2022 at 14:31):From: Corey Richardson <corey@octayn.net>
Dear Isabelle developers,
One minor annoyance when using Isabelle/jEdit is that history navigation
is not local to a text area. In particular, if I create a split and
follow a "hyperlink" via ctrl-click, then go do some work and jump
around in the other split, pressing "back" will undo the navigation I
did in the other split before going back in the split.
Ideally, the navigation commands would act on the currently-focused text
area/pane/window/whatever jargon jEdit uses.
Best,
signature.asc
Email Gateway (Aug 22 2022 at 14:46):From: Makarius <makarius@sketis.net>
The connection of the Isabelle plugin with the Navigator plugin of jEdit
is rather minimal, see
http://isabelle.in.tum.de/repos/isabelle/rev/2d4d9a5f68ff
jEdit actually has its own documentation for the Navigator plugin (see
Help F1). There are some options for the scope: "View Scope" vs.
"EditPane Scope". The description of the latter sounds like what you
have in mind.
The jEdit project http://jedit.org has its own channels to discuss
problems or misunderstandings. Moreover see
http://stackoverflow.com/questions/tagged/jedit
Makarius
signature.asc
Last updated: Apr 26 2024 at 04:17 UTC