support for jEdit Navigator plugin;
authorwenzelm
Fri Apr 04 22:51:22 2014 +0200 (2014-04-04)
changeset 564132d4d9a5f68ff
parent 56412 2dd33da970ea
child 56414 c1bbd3e22226
support for jEdit Navigator plugin;
NEWS
src/Tools/jEdit/src/jEdit.props
src/Tools/jEdit/src/jedit_editor.scala
     1.1 --- a/NEWS	Fri Apr 04 22:21:46 2014 +0200
     1.2 +++ b/NEWS	Fri Apr 04 22:51:22 2014 +0200
     1.3 @@ -108,6 +108,9 @@
     1.4  simplification process, enabled by the newly-introduced
     1.5  "simplifier_trace" declaration.
     1.6  
     1.7 +* Support for Navigator plugin, with toolbar buttons and keyboard
     1.8 +shortcuts similar to major web browsers.
     1.9 +
    1.10  
    1.11  *** Pure ***
    1.12  
     2.1 --- a/src/Tools/jEdit/src/jEdit.props	Fri Apr 04 22:21:46 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/jEdit.props	Fri Apr 04 22:51:22 2014 +0200
     2.3 @@ -227,6 +227,9 @@
     2.4  logo.icon.medium=32x32/apps/isabelle.gif
     2.5  lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
     2.6  match-bracket.shortcut2=C+9
     2.7 +navigator.back.shortcut=A+LEFT
     2.8 +navigator.forward.shortcut=A+RIGHT
     2.9 +navigator.showOnToolbar=true
    2.10  next-bracket.shortcut2=C+e C+9
    2.11  plugin-blacklist.MacOSX.jar=true
    2.12  plugin.MacOSXPlugin.altDispatcher=false
    2.13 @@ -264,7 +267,7 @@
    2.14  view.gutter.selectionAreaWidth=18
    2.15  view.height=787
    2.16  view.middleMousePaste=true
    2.17 -view.showToolbar=false
    2.18 +view.showToolbar=true
    2.19  view.thickCaret=true
    2.20  view.title=Isabelle/jEdit -\u0020
    2.21  view.width=1072
     3.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 04 22:21:46 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 04 22:51:22 2014 +0200
     3.3 @@ -111,10 +111,24 @@
     3.4  
     3.5    /* navigation */
     3.6  
     3.7 +  def push_position(view: View)
     3.8 +  {
     3.9 +    val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
    3.10 +    if (navigator != null) {
    3.11 +      try {
    3.12 +        val m = navigator.getClass.getDeclaredMethod("pushPosition", view.getClass)
    3.13 +        m.invoke(null, view)
    3.14 +      }
    3.15 +      catch { case _: NoSuchMethodException => }
    3.16 +    }
    3.17 +  }
    3.18 +
    3.19    def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
    3.20    {
    3.21      Swing_Thread.require()
    3.22  
    3.23 +    push_position(view)
    3.24 +
    3.25      JEdit_Lib.jedit_buffer(name) match {
    3.26        case Some(buffer) =>
    3.27          view.goToBuffer(buffer)