# HG changeset patch
# User wenzelm
# Date 1406149702 -7200
# Node ID 65fc7ae1bf662c341954c3ed415211cba92e9a5a
# Parent  2288a6f17930bae19f786204f01d39bcb629413c
added action "isabelle.options" (despite problems with initial window size);

diff -r 2288a6f17930 -r 65fc7ae1bf66 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Wed Jul 23 21:02:45 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Wed Jul 23 23:08:22 2014 +0200
@@ -184,6 +184,9 @@
   settings variable @{setting ISABELLE_BUILD_OPTIONS} to change defaults for
   batch builds without affecting Isabelle/jEdit.
 
+  The jEdit action @{action_def isabelle.options} opens the options dialog for
+  the Isabelle plugin; it can be mapped to editor GUI elements as usual.
+
   \medskip Options are usually loaded on startup and saved on shutdown of
   Isabelle/jEdit. Editing the machine-generated @{file_unchecked
   "$ISABELLE_HOME_USER/jedit/properties"} or @{file_unchecked
diff -r 2288a6f17930 -r 65fc7ae1bf66 src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml	Wed Jul 23 21:02:45 2014 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Wed Jul 23 23:08:22 2014 +0200
@@ -122,4 +122,9 @@
 	    isabelle.jedit.Isabelle.reset_dictionary();
 	  </CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.options">
+	  <CODE>
+	    isabelle.jedit.Isabelle.plugin_options(view);
+	  </CODE>
+	</ACTION>
 </ACTIONS>
diff -r 2288a6f17930 -r 65fc7ae1bf66 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Wed Jul 23 21:02:45 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Jul 23 23:08:22 2014 +0200
@@ -9,12 +9,15 @@
 
 import isabelle._
 
+import java.awt.Frame
+
 import scala.swing.CheckBox
 import scala.swing.event.ButtonClicked
 
 import org.gjt.sp.jedit.{jEdit, View, Buffer}
 import org.gjt.sp.jedit.textarea.JEditTextArea
 import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
+import org.gjt.sp.jedit.options.PluginOptions
 
 
 object Isabelle
@@ -314,5 +317,14 @@
       JEdit_Lib.jedit_views().foreach(_.repaint())
     }
   }
+
+
+  /* plugin options */
+
+  def plugin_options(frame: Frame)
+  {
+    GUI_Thread.require {}
+    new org.gjt.sp.jedit.options.PluginOptions(frame, "plugin.isabelle.jedit.Plugin")
+  }
 }
 
diff -r 2288a6f17930 -r 65fc7ae1bf66 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Wed Jul 23 21:02:45 2014 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Wed Jul 23 23:08:22 2014 +0200
@@ -216,6 +216,7 @@
 isabelle.include-word-permanently.label=Include word permanently
 isabelle.exclude-word.label=Exclude word
 isabelle.exclude-word-permanently.label=Exclude word permanently
+isabelle.options.label=Isabelle options
 isabelle.reset-words.label=Reset non-permanent words
 isabelle.reset-continuous-checking.label=Reset continuous checking
 isabelle.reset-font-size.label=Reset font size