src/Pure/System/options.scala

--- 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)
+    }
+  }
+}
+