--- a/src/Tools/jEdit/src/isabelle.scala Tue Aug 25 13:46:24 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Tue Aug 25 16:49:14 2015 +0200
@@ -19,7 +19,7 @@
import org.gjt.sp.jedit.textarea.{JEditTextArea, StructureMatcher}
import org.gjt.sp.jedit.syntax.TokenMarker
import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
-import org.gjt.sp.jedit.options.PluginOptions
+import org.jedit.options.CombinedOptions
object Isabelle
@@ -361,7 +361,7 @@
def plugin_options(frame: Frame)
{
GUI_Thread.require {}
- new org.gjt.sp.jedit.options.PluginOptions(frame, "plugin.isabelle.jedit.Plugin")
+ jEdit.setProperty("Plugin Options.last", "isabelle-general")
+ new CombinedOptions(frame, 1)
}
}
-
--- a/src/Tools/jEdit/src/plugin.scala Tue Aug 25 13:46:24 2015 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Tue Aug 25 16:49:14 2015 +0200
@@ -14,7 +14,6 @@
import scala.swing.{ListView, ScrollPane}
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
-import org.jedit.options.CombinedOptions
import org.gjt.sp.jedit.gui.AboutDialog
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
import org.gjt.sp.jedit.buffer.JEditBuffer