# HG changeset patch
# User wenzelm
# Date 1347299370 -7200
# Node ID ffd9ad9dc35b44e103ae1760f529aab8eae3d720
# Parent  248e66e8321f271c35ea5173aaed2d5c3de92cdf
more detailed option tooltip;
more formal option.load;
properties change propagation to Session_Dockable;

diff -r 248e66e8321f -r ffd9ad9dc35b src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Mon Sep 10 17:13:17 2012 +0200
+++ b/src/Pure/System/options.scala	Mon Sep 10 19:49:30 2012 +0200
@@ -30,8 +30,13 @@
   case object String extends Type
   case object Unknown extends Type
 
-  case class Opt(typ: Type, value: String, description: String)
+  case class Opt(name: String, typ: Type, value: String, description: String)
   {
+    def print: String =
+      "option " + name + " : " + typ.print + " = " +
+        (if (typ == Options.String) quote(value) else value) +
+      (if (description == "") "" else "\n  -- " + quote(description))
+
     def unknown: Boolean = typ == Unknown
   }
 
@@ -124,11 +129,7 @@
 {
   override def toString: String = options.iterator.mkString("Options (", ",", ")")
 
-  def print: String =
-    cat_lines(options.toList.sortBy(_._1).map({ case (name, opt) =>
-      "option " + name + " : " + opt.typ.print + " = " +
-        (if (opt.typ == Options.String) quote(opt.value) else opt.value) +
-      (if (opt.description == "") "" else "\n  -- " + quote(opt.description)) }))
+  def print: String = cat_lines(options.toList.sortBy(_._1).map(p => p._2.print))
 
   def title(strip: String, name: String): String =
   {
@@ -238,7 +239,7 @@
             case "string" => Options.String
             case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name))
           }
-        val opt = Options.Opt(typ, value, description)
+        val opt = Options.Opt(name, typ, value, description)
         (new Options(options + (name -> opt))).check_value(name)
     }
   }
@@ -246,7 +247,7 @@
   def add_permissive(name: String, value: String): Options =
   {
     if (options.isDefinedAt(name)) this + (name, value)
-    else new Options(options + (name -> Options.Opt(Options.Unknown, value, "")))
+    else new Options(options + (name -> Options.Opt(name, Options.Unknown, value, "")))
   }
 
   def + (name: String, value: String): Options =
diff -r 248e66e8321f -r ffd9ad9dc35b src/Tools/jEdit/src/isabelle_logic.scala
--- a/src/Tools/jEdit/src/isabelle_logic.scala	Mon Sep 10 17:13:17 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala	Mon Sep 10 19:49:30 2012 +0200
@@ -37,21 +37,23 @@
 
     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
+      def load: Unit =
+      {
+        val logic = Isabelle.options.string("jedit_logic")
+        entries.find(_.name == logic) match {
+          case Some(entry) => selection.item = entry
+          case None =>
+        }
+      }
+      def save: Unit = Isabelle.options.string("jedit_logic") = selection.item.name
     }
 
+    component.load()
     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.tooltip = Isabelle.options.value.check_name("jedit_logic").print
     component
   }
 
diff -r 248e66e8321f -r ffd9ad9dc35b src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Mon Sep 10 17:13:17 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Mon Sep 10 19:49:30 2012 +0200
@@ -17,6 +17,7 @@
 trait Option_Component extends Component
 {
   val title: String
+  def load(): Unit
   def save(): Unit
 }
 
@@ -35,15 +36,15 @@
       if (opt.typ == Options.Bool)
         new CheckBox with Option_Component {
           val title = opt_title
+          def load = selected = bool(opt_name)
           def save = bool(opt_name) = selected
-          selected = bool(opt_name)
         }
       else {
         val text_area =
           new TextArea with Option_Component {
             val title = opt_title
+            def load = text = value.check_name(opt_name).value
             def save = update(value + (opt_name, text))
-            text = opt.value
           }
         text_area.peer.setInputVerifier(new InputVerifier {
           def verify(jcomponent: JComponent): Boolean =
@@ -56,7 +57,8 @@
           })
         text_area
       }
-    component.tooltip = opt.description
+    component.load()
+    component.tooltip = opt.print
     component
   }
 }
diff -r 248e66e8321f -r ffd9ad9dc35b src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 10 17:13:17 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 10 19:49:30 2012 +0200
@@ -150,6 +150,8 @@
       react {
         case phase: Session.Phase => handle_phase(phase)
 
+        case Session.Global_Settings => Swing_Thread.later { logic.load () }
+
         case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
 
         case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
@@ -160,12 +162,14 @@
   override def init()
   {
     Isabelle.session.phase_changed += main_actor; handle_phase(Isabelle.session.phase)
+    Isabelle.session.global_settings += main_actor
     Isabelle.session.commands_changed += main_actor; handle_update()
   }
 
   override def exit()
   {
     Isabelle.session.phase_changed -= main_actor
+    Isabelle.session.global_settings -= main_actor
     Isabelle.session.commands_changed -= main_actor
   }
 }