# HG changeset patch
# User wenzelm
# Date 1260832881 -3600
# Node ID fcd6a41326a68e5118541ebd462e14dcf5e1dece
# Parent  6c2372c4aefba8a99623a89b54a8629077da75fc
refined treatment of default logic concerning property and GUI;

diff -r 6c2372c4aefb -r fcd6a41326a6 src/Tools/jEdit/src/jedit/isabelle_options.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala	Fri Dec 11 23:38:14 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala	Tue Dec 15 00:21:21 2009 +0100
@@ -17,17 +17,25 @@
   private val logic_name = new JComboBox()
   private val font_size = 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"), {
-      for (name <- "default" :: Isabelle.system.find_logics()) {
-        logic_name.addItem(name)
+      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(name)
+          logic_name.setSelectedItem(item)
       }
       logic_name
     })
+
     addComponent(Isabelle.Property("font-size.title"), {
       font_size.setValue(Isabelle.Int_Property("font-size"))
       font_size
@@ -36,7 +44,7 @@
 
   override def _save()
   {
-    val logic = logic_name.getSelectedItem.asInstanceOf[String]
+    val logic = logic_name.getSelectedItem.asInstanceOf[List_Item].name
     Isabelle.Property("logic") = logic
 
     val size = font_size.getValue().asInstanceOf[Int]
diff -r 6c2372c4aefb -r fcd6a41326a6 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Fri Dec 11 23:38:14 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 15 00:21:21 2009 +0100
@@ -55,17 +55,20 @@
 
   /* settings */
 
-  def cmd_args(): List[String] =
+  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 logic1 = Isabelle.Property("logic")
-      if (logic1 != null && logic1 != "" && logic1 != "default") logic1
-      else {
-        val logic2 = system.getenv("JEDIT_LOGIC")
-        if (logic2 != "") logic2
-        else system.getenv_strict("ISABELLE_LOGIC")
-      }
+      val logic = Isabelle.Property("logic")
+      if (logic != null && logic != "") logic
+      else default_logic()
     }
     modes ++ List(logic)
   }
@@ -94,7 +97,7 @@
     val theory_view = new Theory_View(Isabelle.session, text_area)   // FIXME multiple text areas!?
     mapping += (buffer -> theory_view)
 
-    Isabelle.session.start(Isabelle.cmd_args())
+    Isabelle.session.start(Isabelle.isabelle_args())
     theory_view.activate()
     Isabelle.session.begin_document(buffer.getName)
   }