# HG changeset patch
# User wenzelm
# Date 1368375764 -7200
# Node ID 3301612c48939136e1a0b8343e841da634e5f7e1
# Parent  449fbf64f4a5c838db8a30f418b2d5b8dcc772c8
support for system options as context-sensitive config options;

diff -r 449fbf64f4a5 -r 3301612c4893 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun May 12 18:20:16 2013 +0200
+++ b/src/Pure/ROOT.ML	Sun May 12 18:22:44 2013 +0200
@@ -67,6 +67,8 @@
 
 use "General/graph.ML";
 
+use "System/options.ML";
+
 
 (* concurrency within the ML runtime *)
 
@@ -113,7 +115,6 @@
 use "context.ML";
 use "context_position.ML";
 use "config.ML";
-use "System/options.ML";
 
 
 (* inner syntax *)
diff -r 449fbf64f4a5 -r 3301612c4893 src/Pure/config.ML
--- a/src/Pure/config.ML	Sun May 12 18:20:16 2013 +0200
+++ b/src/Pure/config.ML	Sun May 12 18:22:44 2013 +0200
@@ -27,6 +27,7 @@
   val declare_generic: {global: bool} -> string -> (Context.generic -> value) -> raw
   val declare_global: string -> (Context.generic -> value) -> raw
   val declare: string -> (Context.generic -> value) -> raw
+  val declare_option: string -> raw
   val name_of: 'a T -> string
 end;
 
@@ -138,6 +139,17 @@
 val declare_global = declare_generic {global = true};
 val declare = declare_generic {global = false};
 
+fun declare_option name =
+  let
+    val typ = Options.default_typ name;
+    val default =
+      if typ = Options.boolT then fn _ => Bool (Options.default_bool name)
+      else if typ = Options.intT then fn _ => Int (Options.default_int name)
+      else if typ = Options.realT then fn _ => Real (Options.default_real name)
+      else if typ = Options.stringT then fn _ => String (Options.default_string name)
+      else error ("Unknown type for option " ^ quote name ^ " : " ^ quote typ);
+  in declare name default end;
+
 fun name_of (Config {name, ...}) = name;