src/Pure/System/options.scala

 */
 
 package isabelle
 
 
+import java.util.Locale
 import java.util.Calendar
 
 
 object Options
 {

 
   /* representation */
 
   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
   private case object Real extends Type
   private case object String extends Type

   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 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 */
 
   private def check_name(name: String): Options.Opt =

     Options.PREFS.file renameTo Options.PREFS_BACKUP.file
     File.write(Options.PREFS,
       "(* 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)
+    }
+  }
+}
+