added global config options;
authorwenzelm
Tue Jul 31 00:56:31 2007 +0200 (2007-07-31)
changeset 24077e7ba448bc571
parent 24076 ae946f751c44
child 24078 04b28c723d43
added global config options;
src/Pure/config_option.ML
     1.1 --- a/src/Pure/config_option.ML	Tue Jul 31 00:56:29 2007 +0200
     1.2 +++ b/src/Pure/config_option.ML	Tue Jul 31 00:56:31 2007 +0200
     1.3 @@ -24,6 +24,9 @@
     1.4    val bool: string -> bool -> bool T * (theory -> theory)
     1.5    val int: string -> int -> int T * (theory -> theory)
     1.6    val string: string -> string -> string T * (theory -> theory)
     1.7 +  val global_bool: string -> bool -> bool T * (theory -> theory)
     1.8 +  val global_int: string -> int -> int T * (theory -> theory)
     1.9 +  val global_string: string -> string -> string T * (theory -> theory)
    1.10  end;
    1.11  
    1.12  structure ConfigOption: CONFIG_OPTION =
    1.13 @@ -119,15 +122,24 @@
    1.14      | NONE => error ("Unknown configuration option " ^ quote xname))
    1.15    end;
    1.16  
    1.17 -fun declare make dest name default =
    1.18 +fun declare global make dest name default =
    1.19    let
    1.20      val id = serial ();
    1.21  
    1.22      val default_value = make default;
    1.23      fun get_value context = the_default default_value (Inttab.lookup (Value.get context) id);
    1.24 -    fun map_value f = Value.map (Inttab.map_default (id, default_value) (type_check f));
    1.25 +    fun modify_value f = Value.map (Inttab.map_default (id, default_value) (type_check f));
    1.26 +
    1.27 +    fun map_value f (context as Context.Proof _) =
    1.28 +          let val context' = modify_value f context in
    1.29 +            if global andalso
    1.30 +              get_value (Context.Theory (Context.theory_of context')) <> get_value context'
    1.31 +            then (warning ("Ignoring local change of global option " ^ quote name); context)
    1.32 +            else context'
    1.33 +          end
    1.34 +      | map_value f context = modify_value f context;
    1.35 +
    1.36      val config_value = ConfigOption {get_value = get_value, map_value = map_value};
    1.37 -
    1.38      val config =
    1.39        ConfigOption {get_value = dest o get_value, map_value = fn f => map_value (make o f o dest)};
    1.40      fun setup thy = thy |> Declaration.map (fn tab =>
    1.41 @@ -135,9 +147,13 @@
    1.42          handle Symtab.DUP dup => err_dup_config dup);
    1.43    in (config, setup) end;
    1.44  
    1.45 -val bool = declare Bool (fn Bool b => b);
    1.46 -val int = declare Int (fn Int i => i);
    1.47 -val string = declare String (fn String s => s);
    1.48 +val bool   = declare false Bool (fn Bool b => b);
    1.49 +val int    = declare false Int (fn Int i => i);
    1.50 +val string = declare false String (fn String s => s);
    1.51 +
    1.52 +val global_bool   = declare true Bool (fn Bool b => b);
    1.53 +val global_int    = declare true Int (fn Int i => i);
    1.54 +val global_string = declare true String (fn String s => s);
    1.55  
    1.56  
    1.57  (*final declarations of this structure!*)