separate Isabelle.logic_selector;

--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala	Sat Sep 18 15:50:29 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala	Sat Sep 18 16:05:12 2010 +0200
@@ -14,29 +14,14 @@
 
 class Isabelle_Options extends AbstractOptionPane("isabelle")
 {
-  private val logic_name = new JComboBox()
+  private val logic_selector = Isabelle.logic_selector(Isabelle.Property("logic"))
   private val relative_font_size = new JSpinner()
   private val tooltip_font_size = new JSpinner()
   private val tooltip_dismiss_delay = new JSpinner()
 
-  private class List_Item(val name: String, val descr: String) {
-    def this(name: String) = this(name, name)
-    override def toString = descr
-  }
-
   override def _init()
   {
-    val logic = Isabelle.Property("logic")
-    addComponent(Isabelle.Property("logic.title"), {
-      logic_name.addItem(new List_Item("", "default (" + Isabelle.default_logic() + ")"))
-      for (name <- Isabelle.system.find_logics()) {
-        val item = new List_Item(name)
-        logic_name.addItem(item)
-        if (name == logic)
-          logic_name.setSelectedItem(item)
-      }
-      logic_name
-    })
+    addComponent(Isabelle.Property("logic.title"), logic_selector.peer)
 
     addComponent(Isabelle.Property("relative-font-size.title"), {
       relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100))
@@ -57,7 +42,7 @@
   override def _save()
   {
     Isabelle.Property("logic") =
-      logic_name.getSelectedItem.asInstanceOf[List_Item].name
+      logic_selector.selection.item.name
 
     Isabelle.Int_Property("relative-font-size") =
       relative_font_size.getValue().asInstanceOf[Int]

--- a/src/Tools/jEdit/src/jedit/plugin.scala	Sat Sep 18 15:50:29 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Sat Sep 18 16:05:12 2010 +0200
@@ -14,6 +14,7 @@
 import javax.swing.JTextArea
 
 import scala.collection.mutable
+import scala.swing.ComboBox
 
 import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
   Buffer, EditPane, ServiceManager, View}
@@ -120,27 +121,6 @@
   }
 
 
-  /* settings */
-
-  def default_logic(): String =
-  {
-    val logic = system.getenv("JEDIT_LOGIC")
-    if (logic != "") logic
-    else system.getenv_strict("ISABELLE_LOGIC")
-  }
-
-  def isabelle_args(): List[String] =
-  {
-    val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
-    val logic = {
-      val logic = Property("logic")
-      if (logic != null && logic != "") logic
-      else default_logic()
-    }
-    modes ++ List(logic)
-  }
-
-
   /* main jEdit components */
 
   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
@@ -195,6 +175,45 @@
     }
 
 
+  /* logic image */
+
+  def default_logic(): String =
+  {
+    val logic = system.getenv("JEDIT_LOGIC")
+    if (logic != "") logic
+    else 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() + ")") ::
+        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
+  }
+
+  def isabelle_args(): List[String] =
+  {
+    val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
+    val logic = {
+      val logic = Property("logic")
+      if (logic != null && logic != "") logic
+      else default_logic()
+    }
+    modes ++ List(logic)
+  }
+
+
   /* manage prover */  // FIXME async!?
 
   private def prover_started(view: View): Boolean =