more systematic JEdit_Options.make_component;
separate module Isabelle_Logic;

--- a/src/Pure/System/options.scala	Mon Sep 10 15:20:50 2012 +0200
+++ b/src/Pure/System/options.scala	Mon Sep 10 17:13:17 2012 +0200
@@ -24,11 +24,11 @@
   {
     def print: String = toString.toLowerCase(Locale.ENGLISH)
   }
-  private case object Bool extends Type
-  private case object Int extends Type
-  private case object Real extends Type
-  private case object String extends Type
-  private case object Unknown extends Type
+  case object Bool extends Type
+  case object Int extends Type
+  case object Real extends Type
+  case object String extends Type
+  case object Unknown extends Type
 
   case class Opt(typ: Type, value: String, description: String)
   {
@@ -147,7 +147,7 @@
 
   /* check */
 
-  private def check_name(name: String): Options.Opt =
+  def check_name(name: String): Options.Opt =
     options.get(name) match {
       case Some(opt) if !opt.unknown => opt
       case _ => error("Unknown option " + quote(name))

--- a/src/Tools/jEdit/lib/Tools/jedit	Mon Sep 10 15:20:50 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Sep 10 17:13:17 2012 +0200
@@ -14,6 +14,7 @@
   "src/html_panel.scala"
   "src/hyperlink.scala"
   "src/isabelle_encoding.scala"
+  "src/isabelle_logic.scala"
   "src/isabelle_options.scala"
   "src/isabelle_rendering.scala"
   "src/isabelle_sidekick.scala"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/isabelle_logic.scala	Mon Sep 10 17:13:17 2012 +0200
@@ -0,0 +1,76 @@
+/*  Title:      Tools/jEdit/src/isabelle_logic.scala
+    Author:     Makarius
+
+Isabellel logic session.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.swing.ComboBox
+import scala.swing.event.SelectionChanged
+
+
+object Isabelle_Logic
+{
+  private def default_logic(): String =
+  {
+    val logic = Isabelle_System.getenv("JEDIT_LOGIC")
+    if (logic != "") logic
+    else Isabelle_System.getenv_strict("ISABELLE_LOGIC")
+  }
+
+  private class Logic_Entry(val name: String, val description: String)
+  {
+    override def toString = description
+  }
+
+  def logic_selector(autosave: Boolean): Option_Component =
+  {
+    Swing_Thread.require()
+
+    val entries =
+      new Logic_Entry("", "default (" + default_logic() + ")") ::
+        Isabelle_System.find_logics().map(name => new Logic_Entry(name, name))
+
+    val component = new ComboBox(entries) with Option_Component {
+      val title = Isabelle.options.title("jedit_logic")
+      def save = Isabelle.options.string("jedit_logic") = selection.item.name
+    }
+
+    if (autosave) {
+      component.listenTo(component.selection)
+      component.reactions += { case SelectionChanged(_) => component.save() }
+    }
+
+    val logic = Isabelle.options.string("jedit_logic")
+    entries.find(_.name == logic) match {
+      case Some(entry) => component.selection.item = entry
+      case None =>
+    }
+
+    component.tooltip = Isabelle.options.value.check_name("jedit_logic").description
+    component
+  }
+
+  def session_args(): List[String] =
+  {
+    val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
+    val logic =
+      Isabelle.options.string("jedit_logic") match {
+        case "" => default_logic()
+        case logic => logic
+      }
+    modes ::: List(logic)
+  }
+
+  def session_content(inlined_files: Boolean): Build.Session_Content =
+  {
+    val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
+    val name = Path.explode(session_args().last).base.implode  // FIXME more robust
+    Build.session_content(inlined_files, dirs, name).check_errors
+  }
+}
+

--- a/src/Tools/jEdit/src/isabelle_options.scala	Mon Sep 10 15:20:50 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Mon Sep 10 17:13:17 2012 +0200
@@ -1,5 +1,5 @@
 /*  Title:      Tools/jEdit/src/isabelle_options.scala
-    Author:     Johannes Hölzl, TU Munich
+    Author:     Makarius
 
 Editor pane for plugin options.
 */
@@ -9,59 +9,26 @@
 
 import isabelle._
 
-import javax.swing.{JSpinner, JTextField}
-
-import scala.swing.CheckBox
-
 import org.gjt.sp.jedit.AbstractOptionPane
 
 
 class Isabelle_Options extends AbstractOptionPane("isabelle")
 {
-  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 JTextField()
+  private val components = List(
+    Isabelle_Logic.logic_selector(false),
+    Isabelle.options.make_component("jedit_auto_start"),
+    Isabelle.options.make_component("jedit_relative_font_size"),
+    Isabelle.options.make_component("jedit_tooltip_font_size"),
+    Isabelle.options.make_component("jedit_tooltip_margin"),
+    Isabelle.options.make_component("jedit_tooltip_dismiss_delay"))
 
   override def _init()
   {
-    addComponent(Isabelle.options.title("jedit_logic"),
-      logic_selector.peer.asInstanceOf[java.awt.Component])
-
-    addComponent(Isabelle.options.title("jedit_auto_start"), auto_start.peer)
-    auto_start.selected = Isabelle.options.bool("jedit_auto_start")
-
-    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.options.int("jedit_tooltip_font_size"))
-    addComponent(Isabelle.options.title("jedit_tooltip_font_size"), tooltip_font_size)
-
-    tooltip_margin.setValue(Isabelle.options.int("jedit_tooltip_margin"))
-    addComponent(Isabelle.options.title("jedit_tooltip_margin"), tooltip_margin)
-
-    // 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)
+    for (c <- components) addComponent(c.title, c.peer)
   }
 
   override def _save()
   {
-    Isabelle.options.string("jedit_logic") = logic_selector.selection.item.name
-
-    Isabelle.options.bool("jedit_auto_start") = auto_start.selected
-
-    Isabelle.options.int("jedit_relative_font_size") =
-      relative_font_size.getValue().asInstanceOf[Int]
-
-    Isabelle.options.int("jedit_tooltip_font_size") =
-      tooltip_font_size.getValue().asInstanceOf[Int]
-
-    Isabelle.options.int("jedit_tooltip_margin") =
-      tooltip_margin.getValue().asInstanceOf[Int]
-
-    Isabelle.options + ("jedit_tooltip_dismiss_delay", tooltip_dismiss_delay.getText)
+    for (c <- components) c.save()
   }
 }

--- a/src/Tools/jEdit/src/jedit_options.scala	Mon Sep 10 15:20:50 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Mon Sep 10 17:13:17 2012 +0200
@@ -9,10 +9,55 @@
 
 import isabelle._
 
+import javax.swing.{InputVerifier, JComponent}
+import javax.swing.text.JTextComponent
+import scala.swing.{Component, CheckBox, TextArea}
+
+
+trait Option_Component extends Component
+{
+  val title: String
+  def save(): Unit
+}
 
 class JEdit_Options extends Options_Variable
 {
-  def title(name: String): String = value.title("jedit", name)
-  def description(name: String): String = value.description(name)
+  def title(opt_name: String): String = value.title("jedit", opt_name)
+
+  def make_component(opt_name: String): Option_Component =
+  {
+    Swing_Thread.require()
+
+    val opt = value.check_name(opt_name)
+    val opt_title = title(opt_name)
+
+    val component =
+      if (opt.typ == Options.Bool)
+        new CheckBox with Option_Component {
+          val title = opt_title
+          def save = bool(opt_name) = selected
+          selected = bool(opt_name)
+        }
+      else {
+        val text_area =
+          new TextArea with Option_Component {
+            val title = opt_title
+            def save = update(value + (opt_name, text))
+            text = opt.value
+          }
+        text_area.peer.setInputVerifier(new InputVerifier {
+          def verify(jcomponent: JComponent): Boolean =
+            jcomponent match {
+              case text: JTextComponent =>
+                try { value + (opt_name, text.getText); true }
+                catch { case ERROR(_) => false }
+              case _ => true
+            }
+          })
+        text_area
+      }
+    component.tooltip = opt.description
+    component
+  }
 }
 

--- a/src/Tools/jEdit/src/plugin.scala	Mon Sep 10 15:20:50 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Sep 10 17:13:17 2012 +0200
@@ -14,7 +14,7 @@
 import javax.swing.JOptionPane
 
 import scala.collection.mutable
-import scala.swing.{ComboBox, ListView, ScrollPane}
+import scala.swing.{ListView, ScrollPane}
 
 import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
   Buffer, EditPane, ServiceManager, View}
@@ -227,53 +227,6 @@
     }
 
 
-  /* logic image */
-
-  def default_logic(): String =
-  {
-    val logic = Isabelle_System.getenv("JEDIT_LOGIC")
-    if (logic != "") logic
-    else Isabelle_System.getenv_strict("ISABELLE_LOGIC")
-  }
-
-  class Logic_Entry(val name: String, val description: String)
-  {
-    override def toString = description
-  }
-
-  def logic_selector(logic: String): ComboBox[Logic_Entry] =
-  {
-    val entries =
-      new Logic_Entry("", "default (" + default_logic() + ")") ::
-        Isabelle_System.find_logics().map(name => new Logic_Entry(name, name))
-    val component = new ComboBox(entries)
-    entries.find(_.name == logic) match {
-      case None =>
-      case Some(entry) => component.selection.item = entry
-    }
-    component.tooltip = "Isabelle logic image"
-    component
-  }
-
-  def session_args(): List[String] =
-  {
-    val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
-    val logic =
-      Isabelle.options.string("jedit_logic") match {
-        case "" => Isabelle.default_logic()
-        case logic => logic
-      }
-    modes ::: List(logic)
-  }
-
-  def session_content(inlined_files: Boolean): Build.Session_Content =
-  {
-    val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
-    val name = Path.explode(session_args().last).base.implode  // FIXME more robust
-    Build.session_content(inlined_files, dirs, name).check_errors
-  }
-
-
   /* convenience actions */
 
   private def user_input(text_area: JEditTextArea, s1: String, s2: String = "")
@@ -398,7 +351,7 @@
       message match {
         case msg: EditorStarted =>
           if (Isabelle.options.bool("jedit_auto_start"))
-            Isabelle.session.start(Isabelle.session_args())
+            Isabelle.session.start(Isabelle_Logic.session_args())
 
         case msg: BufferUpdate
         if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
@@ -452,7 +405,7 @@
       if (ModeProvider.instance.isInstanceOf[ModeProvider])
         ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
 
-      val content = Isabelle.session_content(false)
+      val content = Isabelle_Logic.session_content(false)
       val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
       Isabelle.session = new Session(thy_load)
 

--- a/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 10 15:20:50 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 10 17:13:17 2012 +0200
@@ -11,7 +11,7 @@
 
 import scala.actors.Actor._
 import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component}
-import scala.swing.event.{ButtonClicked, MouseClicked, SelectionChanged}
+import scala.swing.event.{ButtonClicked, MouseClicked}
 
 import java.lang.System
 import java.awt.{BorderLayout, Graphics2D, Insets}
@@ -60,12 +60,7 @@
   }
   check.tooltip = jEdit.getProperty("isabelle.check-buffer.label")
 
-  private val logic = Isabelle.logic_selector(Isabelle.options.string("jedit_logic"))
-  logic.listenTo(logic.selection)
-  logic.reactions += {
-    case SelectionChanged(_) =>
-      Isabelle.options.string("jedit_logic") = logic.selection.item.name
-  }
+  private val logic = Isabelle_Logic.logic_selector(true)
 
   private val controls =
     new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic)