# HG changeset patch
# User wenzelm
# Date 1415481016 -3600
# Node ID 8b7caf447357f072adb5875f67d2d0663e0aadf9
# Parent  d07464875dd41ff257fc835bdd12013477cee64e
removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);

diff -r d07464875dd4 -r 8b7caf447357 src/Pure/config.ML
--- a/src/Pure/config.ML	Sat Nov 08 21:31:51 2014 +0100
+++ b/src/Pure/config.ML	Sat Nov 08 22:10:16 2014 +0100
@@ -25,9 +25,7 @@
   val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
   val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
   val declare: string * Position.T -> (Context.generic -> value) -> raw
-  val declare_global: string * Position.T -> (Context.generic -> value) -> raw
   val declare_option: string * Position.T -> raw
-  val declare_option_global: string * Position.T -> raw
   val name_of: 'a T -> string
   val pos_of: 'a T -> Position.T
 end;
@@ -113,9 +111,7 @@
   fun merge data = Inttab.merge (K true) data;
 );
 
-local
-
-fun declare_generic global (name, pos) default =
+fun declare (name, pos) default =
   let
     val id = serial ();
 
@@ -124,22 +120,13 @@
         SOME value => value
       | NONE => default context);
 
-    fun update_value f context =
+    fun map_value f context =
       Value.map (Inttab.update (id, type_check (name, pos) f (get_value context))) context;
+  in
+    Config {name = name, pos = pos, get_value = get_value, map_value = map_value}
+  end;
 
-    fun map_value f (context as Context.Proof ctxt) =
-          let val context' = update_value f context in
-            if global andalso
-              Context_Position.is_really_visible ctxt andalso
-              print_value (get_value (Context.Theory (Context.theory_of context'))) <>
-                print_value (get_value context')
-            then (warning ("Ignoring local change of global option " ^ quote name); context)
-            else context'
-          end
-      | map_value f context = update_value f context;
-  in Config {name = name, pos = pos, get_value = get_value, map_value = map_value} end;
-
-fun declare_option_generic global (name, pos) =
+fun declare_option (name, pos) =
   let
     val typ = Options.default_typ name;
     val default =
@@ -148,16 +135,7 @@
       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 ^ Position.here pos ^ " : " ^ quote typ);
-  in declare_generic global (name, pos) default end;
-
-in
-
-val declare = declare_generic false;
-val declare_global = declare_generic true;
-val declare_option = declare_option_generic false;
-val declare_option_global = declare_option_generic true;
-
-end;
+  in declare (name, pos) default end;
 
 fun name_of (Config {name, ...}) = name;
 fun pos_of (Config {pos, ...}) = pos;