manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);

--- a/src/Pure/System/options.scala	Mon Sep 10 13:19:56 2012 +0200
+++ b/src/Pure/System/options.scala	Mon Sep 10 15:20:50 2012 +0200
@@ -7,6 +7,7 @@
 package isabelle
 
 
+import java.util.Locale
 import java.util.Calendar
 
 
@@ -21,7 +22,7 @@
 
   sealed abstract class Type
   {
-    def print: String = toString.toLowerCase
+    def print: String = toString.toLowerCase(Locale.ENGLISH)
   }
   private case object Bool extends Type
   private case object Int extends Type
@@ -129,6 +130,20 @@
         (if (opt.typ == Options.String) quote(opt.value) else opt.value) +
       (if (opt.description == "") "" else "\n  -- " + quote(opt.description)) }))
 
+  def title(strip: String, name: String): String =
+  {
+    check_name(name)
+    val words = space_explode('_', name)
+    val words1 =
+      words match {
+        case word :: rest if word == strip => rest
+        case _ => words
+      }
+    words1.map(Library.capitalize).mkString(" ")
+  }
+
+  def description(name: String): String = check_name(name).description
+
 
   /* check */
 
@@ -302,3 +317,64 @@
       "(* generated by Isabelle " + Calendar.getInstance.getTime + " *)\n\n" + prefs)
   }
 }
+
+
+class Options_Variable
+{
+  // owned by Swing thread
+  @volatile private var options = Options.empty
+
+  def value: Options = options
+  def update(new_options: Options)
+  {
+    Swing_Thread.require()
+    options = new_options
+  }
+
+  def + (name: String, x: String)
+  {
+    Swing_Thread.require()
+    options = options + (name, x)
+  }
+
+  val bool = new Object
+  {
+    def apply(name: String): Boolean = options.bool(name)
+    def update(name: String, x: Boolean)
+    {
+      Swing_Thread.require()
+      options = options.bool.update(name, x)
+    }
+  }
+
+  val int = new Object
+  {
+    def apply(name: String): Int = options.int(name)
+    def update(name: String, x: Int)
+    {
+      Swing_Thread.require()
+      options = options.int.update(name, x)
+    }
+  }
+
+  val real = new Object
+  {
+    def apply(name: String): Double = options.real(name)
+    def update(name: String, x: Double)
+    {
+      Swing_Thread.require()
+      options = options.real.update(name, x)
+    }
+  }
+
+  val string = new Object
+  {
+    def apply(name: String): String = options.string(name)
+    def update(name: String, x: String)
+    {
+      Swing_Thread.require()
+      options = options.string.update(name, x)
+    }
+  }
+}
+

--- a/src/Pure/library.scala	Mon Sep 10 13:19:56 2012 +0200
+++ b/src/Pure/library.scala	Mon Sep 10 15:20:50 2012 +0200
@@ -9,6 +9,7 @@
 
 
 import java.lang.System
+import java.util.Locale
 import java.awt.Component
 import javax.swing.JOptionPane
 
@@ -84,6 +85,10 @@
     if (str.endsWith("\n")) str.substring(0, str.length - 1)
     else str
 
+  def capitalize(str: String): String =
+    if (str.length == 0) str
+    else str.substring(0, 1).toUpperCase(Locale.ENGLISH) + str.substring(1)
+
 
   /* quote */
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/etc/options	Mon Sep 10 15:20:50 2012 +0200
@@ -0,0 +1,19 @@
+(* :mode=isabelle-options: *)
+
+option jedit_logic : string = ""
+  -- "default logic session"
+
+option jedit_auto_start : bool = true
+  -- "auto-start prover session on editor startup"
+
+option jedit_relative_font_size : int = 100
+  -- "relative font size of output panel wrt. main text area"
+
+option jedit_tooltip_font_size : int = 10
+  -- "tooltip font size (according to HTML)"
+
+option jedit_tooltip_margin : int = 60
+  -- "margin for tooltip pretty-printing (in characters)"
+
+option jedit_tooltip_dismiss_delay : real = 8.0
+  -- "global delay for Swing tooltips (in seconds)"

--- a/src/Tools/jEdit/lib/Tools/jedit	Mon Sep 10 13:19:56 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Sep 10 15:20:50 2012 +0200
@@ -18,6 +18,7 @@
   "src/isabelle_rendering.scala"
   "src/isabelle_sidekick.scala"
   "src/jedit_thy_load.scala"
+  "src/jedit_options.scala"
   "src/output_dockable.scala"
   "src/plugin.scala"
   "src/protocol_dockable.scala"

--- a/src/Tools/jEdit/src/Isabelle.props	Mon Sep 10 13:19:56 2012 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props	Mon Sep 10 15:20:50 2012 +0200
@@ -23,17 +23,6 @@
 plugin.isabelle.jedit.Plugin.option-pane=isabelle
 options.isabelle.label=Isabelle
 options.isabelle.code=new isabelle.jedit.Isabelle_Options();
-options.isabelle.logic.title=Logic
-options.isabelle.relative-font-size.title=Relative Font Size
-options.isabelle.relative-font-size=100
-options.isabelle.tooltip-font-size.title=Tooltip Font Size
-options.isabelle.tooltip-font-size=10
-options.isabelle.tooltip-margin.title=Tooltip Margin
-options.isabelle.tooltip-margin=60
-options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
-options.isabelle.tooltip-dismiss-delay=8.0
-options.isabelle.auto-start.title=Auto Start
-options.isabelle.auto-start=true
 
 #actions
 isabelle.check-buffer.label=Commence full proof checking of current buffer

--- a/src/Tools/jEdit/src/isabelle_options.scala	Mon Sep 10 13:19:56 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Mon Sep 10 15:20:50 2012 +0200
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import javax.swing.JSpinner
+import javax.swing.{JSpinner, JTextField}
 
 import scala.swing.CheckBox
 
@@ -18,51 +18,50 @@
 
 class Isabelle_Options extends AbstractOptionPane("isabelle")
 {
-  private val logic_selector = Isabelle.logic_selector(Isabelle.Property("logic"))
+  private val logic_selector = Isabelle.logic_selector(Isabelle.options.string("jedit_logic"))
   private val auto_start = new CheckBox()
   private val relative_font_size = new JSpinner()
   private val tooltip_font_size = new JSpinner()
   private val tooltip_margin = new JSpinner()
-  private val tooltip_dismiss_delay = new JSpinner()
+  private val tooltip_dismiss_delay = new JTextField()
 
   override def _init()
   {
-    addComponent(Isabelle.Property("logic.title"),
+    addComponent(Isabelle.options.title("jedit_logic"),
       logic_selector.peer.asInstanceOf[java.awt.Component])
 
-    addComponent(Isabelle.Property("auto-start.title"), auto_start.peer)
-    auto_start.selected = Isabelle.Boolean_Property("auto-start")
+    addComponent(Isabelle.options.title("jedit_auto_start"), auto_start.peer)
+    auto_start.selected = Isabelle.options.bool("jedit_auto_start")
 
-    relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100))
-    addComponent(Isabelle.Property("relative-font-size.title"), relative_font_size)
+    addComponent(Isabelle.options.title("jedit_relative_font_size"), relative_font_size)
+    relative_font_size.setValue(Isabelle.options.int("jedit_relative_font_size"))
 
-    tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
-    addComponent(Isabelle.Property("tooltip-font-size.title"), tooltip_font_size)
+    tooltip_font_size.setValue(Isabelle.options.int("jedit_tooltip_font_size"))
+    addComponent(Isabelle.options.title("jedit_tooltip_font_size"), tooltip_font_size)
 
-    tooltip_margin.setValue(Isabelle.Int_Property("tooltip-margin", 40))
-    addComponent(Isabelle.Property("tooltip-margin.title"), tooltip_margin)
+    tooltip_margin.setValue(Isabelle.options.int("jedit_tooltip_margin"))
+    addComponent(Isabelle.options.title("jedit_tooltip_margin"), tooltip_margin)
 
-    tooltip_dismiss_delay.setValue(
-      Isabelle.Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)).ms.toInt)
-    addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay)
+    // FIXME InputVerifier for Double
+    tooltip_dismiss_delay.setText(Isabelle.options.real("jedit_tooltip_dismiss_delay").toString)
+    addComponent(Isabelle.options.title("jedit_tooltip_dismiss_delay"), tooltip_dismiss_delay)
   }
 
   override def _save()
   {
-    Isabelle.Property("logic") = logic_selector.selection.item.name
+    Isabelle.options.string("jedit_logic") = logic_selector.selection.item.name
 
-    Isabelle.Boolean_Property("auto-start") = auto_start.selected
+    Isabelle.options.bool("jedit_auto_start") = auto_start.selected
 
-    Isabelle.Int_Property("relative-font-size") =
+    Isabelle.options.int("jedit_relative_font_size") =
       relative_font_size.getValue().asInstanceOf[Int]
 
-    Isabelle.Int_Property("tooltip-font-size") =
+    Isabelle.options.int("jedit_tooltip_font_size") =
       tooltip_font_size.getValue().asInstanceOf[Int]
 
-    Isabelle.Int_Property("tooltip-margin") =
+    Isabelle.options.int("jedit_tooltip_margin") =
       tooltip_margin.getValue().asInstanceOf[Int]
 
-    Isabelle.Time_Property("tooltip-dismiss-delay") =
-      Time.ms(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
+    Isabelle.options + ("jedit_tooltip_dismiss_delay", tooltip_dismiss_delay.getText)
   }
 }

--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Mon Sep 10 13:19:56 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Mon Sep 10 15:20:50 2012 +0200
@@ -151,7 +151,7 @@
 
 
   private def tooltip_text(msg: XML.Tree): String =
-    Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))
+    Pretty.string_of(List(msg), margin = Isabelle.options.int("jedit_tooltip_margin"))
 
   def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
   {
@@ -195,7 +195,7 @@
 
   private def string_of_typing(kind: String, body: XML.Body): String =
     Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
-      margin = Isabelle.Int_Property("tooltip-margin"))
+      margin = Isabelle.options.int("jedit_tooltip_margin"))
 
   def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
   {

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit_options.scala	Mon Sep 10 15:20:50 2012 +0200
@@ -0,0 +1,18 @@
+/*  Title:      Tools/jEdit/src/jedit_options.scala
+    Author:     Makarius
+
+Options for Isabelle/jEdit.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+
+class JEdit_Options extends Options_Variable
+{
+  def title(name: String): String = value.title("jedit", name)
+  def description(name: String): String = value.description(name)
+}
+

--- a/src/Tools/jEdit/src/plugin.scala	Mon Sep 10 13:19:56 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Sep 10 15:20:50 2012 +0200
@@ -34,6 +34,8 @@
 {
   /* plugin instance */
 
+  val options = new JEdit_Options
+
   @volatile var startup_failure: Option[Throwable] = None
   @volatile var startup_notified = false
 
@@ -51,81 +53,26 @@
   }
 
 
-  /* properties */
-
-  val OPTION_PREFIX = "options.isabelle."
-
-  object Property
-  {
-    def apply(name: String): String =
-      jEdit.getProperty(OPTION_PREFIX + name)
-    def apply(name: String, default: String): String =
-      jEdit.getProperty(OPTION_PREFIX + name, default)
-    def update(name: String, value: String) =
-      jEdit.setProperty(OPTION_PREFIX + name, value)
-  }
-
-  object Boolean_Property
-  {
-    def apply(name: String): Boolean =
-      jEdit.getBooleanProperty(OPTION_PREFIX + name)
-    def apply(name: String, default: Boolean): Boolean =
-      jEdit.getBooleanProperty(OPTION_PREFIX + name, default)
-    def update(name: String, value: Boolean) =
-      jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
-  }
-
-  object Int_Property
-  {
-    def apply(name: String): Int =
-      jEdit.getIntegerProperty(OPTION_PREFIX + name)
-    def apply(name: String, default: Int): Int =
-      jEdit.getIntegerProperty(OPTION_PREFIX + name, default)
-    def update(name: String, value: Int) =
-      jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
-  }
-
-  object Double_Property
-  {
-    def apply(name: String): Double =
-      jEdit.getDoubleProperty(OPTION_PREFIX + name, 0.0)
-    def apply(name: String, default: Double): Double =
-      jEdit.getDoubleProperty(OPTION_PREFIX + name, default)
-    def update(name: String, value: Double) =
-      jEdit.setDoubleProperty(OPTION_PREFIX + name, value)
-  }
-
-  object Time_Property
-  {
-    def apply(name: String): Time =
-      Time.seconds(Double_Property(name))
-    def apply(name: String, default: Time): Time =
-      Time.seconds(Double_Property(name, default.seconds))
-    def update(name: String, value: Time) =
-      Double_Property.update(name, value.seconds)
-  }
-
-
   /* font */
 
   def font_family(): String = jEdit.getProperty("view.font")
 
   def font_size(): Float =
     (jEdit.getIntegerProperty("view.fontsize", 16) *
-      Int_Property("relative-font-size", 100)).toFloat / 100
+      options.int("jedit_relative_font_size")).toFloat / 100
 
 
   /* tooltip markup */
 
   def tooltip(text: String): String =
     "<html><pre style=\"font-family: " + font_family() + "; font-size: " +
-        Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)
+        options.int("jedit_tooltip_font_size").toString + "px; \">" +  // FIXME proper scaling (!?)
       HTML.encode(text) + "</pre></html>"
 
   private val tooltip_lb = Time.seconds(0.5)
   private val tooltip_ub = Time.seconds(60.0)
   def tooltip_dismiss_delay(): Time =
-    Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max tooltip_lb min tooltip_ub
+    Time.seconds(options.real("jedit_tooltip_dismiss_delay")) max tooltip_lb min tooltip_ub
 
   def setup_tooltips()
   {
@@ -311,11 +258,11 @@
   def session_args(): List[String] =
   {
     val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
-    val logic = {
-      val logic = Property("logic")
-      if (logic != null && logic != "") logic
-      else Isabelle.default_logic()
-    }
+    val logic =
+      Isabelle.options.string("jedit_logic") match {
+        case "" => Isabelle.default_logic()
+        case logic => logic
+      }
     modes ::: List(logic)
   }
 
@@ -450,7 +397,7 @@
     if (Isabelle.startup_failure.isEmpty) {
       message match {
         case msg: EditorStarted =>
-          if (Isabelle.Boolean_Property("auto-start"))
+          if (Isabelle.options.bool("jedit_auto_start"))
             Isabelle.session.start(Isabelle.session_args())
 
         case msg: BufferUpdate
@@ -492,10 +439,15 @@
   {
     try {
       Isabelle.plugin = this
-      Isabelle.setup_tooltips()
       Isabelle_System.init()
       Isabelle_System.install_fonts()
 
+      val init_options = Options.init()
+      Swing_Thread.now {
+        Isabelle.options.update(init_options)
+        Isabelle.setup_tooltips()
+      }
+
       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
       if (ModeProvider.instance.isInstanceOf[ModeProvider])
         ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
@@ -516,6 +468,9 @@
 
   override def stop()
   {
+    if (Isabelle.startup_failure.isEmpty)
+      Isabelle.options.value.save_prefs()
+
     Isabelle.session.phase_changed -= session_manager
     Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
     Isabelle.session.stop()

--- a/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 10 13:19:56 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 10 15:20:50 2012 +0200
@@ -60,10 +60,11 @@
   }
   check.tooltip = jEdit.getProperty("isabelle.check-buffer.label")
 
-  private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
+  private val logic = Isabelle.logic_selector(Isabelle.options.string("jedit_logic"))
   logic.listenTo(logic.selection)
   logic.reactions += {
-    case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
+    case SelectionChanged(_) =>
+      Isabelle.options.string("jedit_logic") = logic.selection.item.name
   }
 
   private val controls =