added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);

--- a/src/Pure/IsaMakefile	Mon Jul 23 21:01:16 2012 +0200
+++ b/src/Pure/IsaMakefile	Mon Jul 23 22:35:10 2012 +0200
@@ -188,11 +188,12 @@
   Syntax/syntax_phases.ML				\
   Syntax/syntax_trans.ML				\
   Syntax/term_position.ML				\
+  System/build.ML					\
   System/invoke_scala.ML				\
-  System/build.ML					\
   System/isabelle_process.ML				\
   System/isabelle_system.ML				\
   System/isar.ML					\
+  System/options.ML					\
   System/session.ML					\
   System/system_channel.ML				\
   Thy/html.ML						\

--- a/src/Pure/ROOT.ML	Mon Jul 23 21:01:16 2012 +0200
+++ b/src/Pure/ROOT.ML	Mon Jul 23 22:35:10 2012 +0200
@@ -103,6 +103,7 @@
 use "context.ML";
 use "context_position.ML";
 use "config.ML";
+use "System/options.ML";
 
 
 (* inner syntax *)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/options.ML	Mon Jul 23 22:35:10 2012 +0200
@@ -0,0 +1,76 @@
+(*  Title:      Pure/System/options.ML
+    Author:     Makarius
+
+Stand-alone options with external string representation.
+*)
+
+signature OPTIONS =
+sig
+  type T
+  val empty: T
+  val bool: T -> string -> bool
+  val int: T -> string -> int
+  val real: T -> string -> real
+  val string: T -> string -> string
+  val declare: {name: string, typ: string, value: string} -> T -> T
+  val decode: XML.body -> T
+end;
+
+structure Options: OPTIONS =
+struct
+
+(* representation *)
+
+val boolT = "bool";
+val intT = "int";
+val realT = "real";
+val stringT = "string";
+
+datatype T = Options of {typ: string, value: string} Symtab.table;
+
+val empty = Options Symtab.empty;
+
+
+(* get *)
+
+fun get T parse (Options tab) name =
+  (case Symtab.lookup tab name of
+    SOME {typ, value} =>
+      if typ = T then
+        (case parse value of
+          SOME x => x
+        | NONE =>
+            error ("Malformed value for option " ^ quote name ^ " : " ^ T ^ " =\n" ^ quote value))
+      else error ("Ill-typed option " ^ quote name ^ " : " ^ typ ^ " vs. " ^ T)
+  | NONE => error ("Unknown option " ^ quote name));
+
+val bool = get boolT Bool.fromString;
+val int = get intT Int.fromString;
+val real = get realT Real.fromString;
+val string = get stringT SOME;
+
+
+(* declare *)
+
+fun declare {name, typ, value} (Options tab) =
+  let
+    val check_value =
+      if typ = boolT then ignore oo bool
+      else if typ = intT then ignore oo int
+      else if typ = realT then ignore oo real
+      else if typ = stringT then ignore oo string
+      else error ("Unknown type for option " ^ quote name ^ " : " ^ quote typ);
+    val options' = Options (Symtab.update_new (name, {typ = typ, value = value}) tab)
+      handle Symtab.DUP _ => error ("Duplicate declaration of option " ^ quote name);
+    val _ = check_value options' name;
+  in options' end;
+
+
+(* decode *)
+
+fun decode body =
+  fold (declare o (fn (name, typ, value) => {name = name, typ = typ, value = value}))
+    (let open XML.Decode in list (triple string string string) end body) empty;
+
+end;
+

--- a/src/Pure/System/options.scala	Mon Jul 23 21:01:16 2012 +0200
+++ b/src/Pure/System/options.scala	Mon Jul 23 22:35:10 2012 +0200
@@ -177,7 +177,7 @@
             case "int" => Options.Int
             case "real" => Options.Real
             case "string" => Options.String
-            case _ => error("Malformed type for option " + quote(name) + " : " + quote(typ_name))
+            case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name))
           }
         (new Options(options + (name -> Options.Opt(typ, value, description)))).check_value(name)
     }
@@ -209,4 +209,14 @@
       case i => define(str.substring(0, i), str.substring(i + 1))
     }
   }
+
+
+  /* encode */
+
+  def encode: XML.Body =
+  {
+    import XML.Encode.{string => str, _}
+    list(triple(str, str, str))(
+      options.toList.map({ case (name, opt) => (name, opt.typ.print, opt.value) }))
+  }
 }