# HG changeset patch
# User wenzelm
# Date 1396644682 -7200
# Node ID 2d4d9a5f68ff191c96e66897f4af847309dc426d
# Parent  2dd33da970ea63376e719e6b4793f9393bcb93eb
support for jEdit Navigator plugin;

diff -r 2dd33da970ea -r 2d4d9a5f68ff NEWS
--- 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 ***
 
diff -r 2dd33da970ea -r 2d4d9a5f68ff src/Tools/jEdit/src/jEdit.props
--- 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
diff -r 2dd33da970ea -r 2d4d9a5f68ff src/Tools/jEdit/src/jedit_editor.scala
--- 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)