--- a/NEWS Fri Apr 04 22:21:46 2014 +0200
+++ b/NEWS Fri Apr 04 22:51:22 2014 +0200
@@ -108,6 +108,9 @@
simplification process, enabled by the newly-introduced
"simplifier_trace" declaration.
+* Support for Navigator plugin, with toolbar buttons and keyboard
+shortcuts similar to major web browsers.
+
*** Pure ***
--- a/src/Tools/jEdit/src/jEdit.props Fri Apr 04 22:21:46 2014 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Fri Apr 04 22:51:22 2014 +0200
@@ -227,6 +227,9 @@
logo.icon.medium=32x32/apps/isabelle.gif
lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
match-bracket.shortcut2=C+9
+navigator.back.shortcut=A+LEFT
+navigator.forward.shortcut=A+RIGHT
+navigator.showOnToolbar=true
next-bracket.shortcut2=C+e C+9
plugin-blacklist.MacOSX.jar=true
plugin.MacOSXPlugin.altDispatcher=false
@@ -264,7 +267,7 @@
view.gutter.selectionAreaWidth=18
view.height=787
view.middleMousePaste=true
-view.showToolbar=false
+view.showToolbar=true
view.thickCaret=true
view.title=Isabelle/jEdit -\u0020
view.width=1072
--- a/src/Tools/jEdit/src/jedit_editor.scala Fri Apr 04 22:21:46 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Fri Apr 04 22:51:22 2014 +0200
@@ -111,10 +111,24 @@
/* navigation */
+ def push_position(view: View)
+ {
+ val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
+ if (navigator != null) {
+ try {
+ val m = navigator.getClass.getDeclaredMethod("pushPosition", view.getClass)
+ m.invoke(null, view)
+ }
+ catch { case _: NoSuchMethodException => }
+ }
+ }
+
def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
{
Swing_Thread.require()
+ push_position(view)
+
JEdit_Lib.jedit_buffer(name) match {
case Some(buffer) =>
view.goToBuffer(buffer)