--- a/src/Pure/IsaMakefile Fri Jul 27 20:11:49 2007 +0200
+++ b/src/Pure/IsaMakefile Fri Jul 27 21:55:17 2007 +0200
@@ -63,13 +63,13 @@
Tools/codegen_package.ML Tools/codegen_serializer.ML Tools/codegen_thingol.ML \
Tools/invoke.ML Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML \
Tools/xml.ML Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML \
- compress.ML config.ML conjunction.ML consts.ML context.ML context_position.ML \
- conv.ML defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML \
- install_pp.ML library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML \
- name.ML net.ML old_goals.ML pattern.ML proofterm.ML pure_setup.ML pure_thy.ML \
- search.ML sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML \
- term.ML term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML \
- variable.ML
+ compress.ML config_option.ML conjunction.ML consts.ML context.ML \
+ context_position.ML conv.ML defs.ML display.ML drule.ML envir.ML \
+ fact_index.ML goal.ML install_pp.ML library.ML logic.ML meta_simplifier.ML \
+ more_thm.ML morphism.ML name.ML net.ML old_goals.ML pattern.ML proofterm.ML \
+ pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML \
+ tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML \
+ type_infer.ML unify.ML variable.ML
@./mk
--- a/src/Pure/ROOT.ML Fri Jul 27 20:11:49 2007 +0200
+++ b/src/Pure/ROOT.ML Fri Jul 27 21:55:17 2007 +0200
@@ -41,7 +41,7 @@
use "Syntax/printer.ML";
use "Syntax/syntax.ML";
-use "config.ML";
+use "config_option.ML";
use "General/ml_syntax.ML";
(*core of tactical proof system*)
--- a/src/Pure/config.ML Fri Jul 27 20:11:49 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,134 +0,0 @@
-(* Title: Pure/config.ML
- ID: $Id$
- Author: Makarius
-
-Configuration options as values within the local context. Global
-environment of named options, with type declaration.
-*)
-
-signature CONFIG =
-sig
- datatype value = Bool of bool | Int of int | String of string
- type 'a T
- val get: Proof.context -> 'a T -> 'a
- val get_thy: theory -> 'a T -> 'a
- val get_generic: Context.generic -> 'a T -> 'a
- val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
- val map_thy: 'a T -> ('a -> 'a) -> theory -> theory
- val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
- val put: 'a T -> 'a -> Proof.context -> Proof.context
- val put_thy: 'a T -> 'a -> theory -> theory
- val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
- val print_configs: Proof.context -> unit
- val the_config: string -> value T * value
- val bool: string -> bool -> bool T
- val int: string -> int -> int T
- val string: string -> string -> string T
-end;
-
-structure Config: CONFIG =
-struct
-
-(* mixed values *)
-
-datatype value =
- Bool of bool |
- Int of int |
- String of string;
-
-fun print_value (Bool true) = "true"
- | print_value (Bool false) = "false"
- | print_value (Int i) = signed_string_of_int i
- | print_value (String s) = quote s;
-
-fun print_type (Bool _) = "boolean"
- | print_type (Int _) = "integer"
- | print_type (String _) = "string";
-
-fun same_type (Bool _) (Bool _) = true
- | same_type (Int _) (Int _) = true
- | same_type (String _) (String _) = true
- | same_type _ _ = false;
-
-fun type_check f value =
- let
- val value' = f value;
- val _ = same_type value value' orelse
- error ("Ill-typed configuration option: " ^ print_type value ^
- " expected,\nbut " ^ print_type value' ^ " was found");
- in value' end;
-
-structure ConfigData = GenericDataFun
-(
- type T = value Inttab.table;
- val empty = Inttab.empty;
- val extend = I;
- fun merge _ = Inttab.merge (K true);
-);
-
-
-(* abstract configuration options *)
-
-datatype 'a T = Config of
- {get_value: Context.generic -> 'a,
- map_value: ('a -> 'a) -> Context.generic -> Context.generic};
-
-fun get_generic context (Config {get_value, ...}) = get_value context;
-fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
-fun get_thy thy = get_generic (Context.Theory thy);
-
-fun map_generic (Config {map_value, ...}) f context = map_value f context;
-fun map_ctxt config f = Context.proof_map (map_generic config f);
-fun map_thy config f = Context.theory_map (map_generic config f);
-
-fun put_generic config value = map_generic config (K value);
-fun put_ctxt config value = map_ctxt config (K value);
-fun put_thy config value = map_thy config (K value);
-
-
-(* global declarations *)
-
-local val global_configs = ref (Symtab.empty: (value T * value) Symtab.table) in
-
-fun print_configs ctxt =
- let
- fun prt (name, (config, default)) =
- Pretty.block [Pretty.str (name ^ ": " ^ print_type default ^ " ="), Pretty.brk 1,
- Pretty.str (print_value (get_ctxt ctxt config))];
- val configs = sort_wrt #1 (Symtab.dest (! global_configs));
- in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
-
-fun the_config name =
- (case Symtab.lookup (! global_configs) name of SOME cfg => cfg
- | NONE => error ("Unknown configuration option " ^ quote name));
-
-fun declare make dest name default =
- let
- val id = serial ();
-
- val default_value = make default;
- fun get_value context =
- the_default default_value (Inttab.lookup (ConfigData.get context) id);
- fun map_value f = ConfigData.map (Inttab.map_default (id, default_value) (type_check f));
- val config_value = Config {get_value = get_value, map_value = map_value};
-
- val _ = CRITICAL (fn () =>
- (if Symtab.defined (! global_configs) name
- then warning ("Hiding existing configuration option " ^ quote name) else ();
- change global_configs (Symtab.update (name, (config_value, default_value)))));
-
- in Config {get_value = dest o get_value, map_value = fn f => map_value (make o f o dest)} end;
-
-end;
-
-val bool = declare Bool (fn Bool b => b);
-val int = declare Int (fn Int i => i);
-val string = declare String (fn String s => s);
-
-
-(*final declarations of this structure!*)
-val get = get_ctxt;
-val map = map_ctxt;
-val put = put_ctxt;
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/config_option.ML Fri Jul 27 21:55:17 2007 +0200
@@ -0,0 +1,136 @@
+(* Title: Pure/config_option.ML
+ ID: $Id$
+ Author: Makarius
+
+Configuration options as values within the local context. Global
+environment of named options, with type declaration.
+*)
+
+signature CONFIG_OPTION =
+sig
+ datatype value = Bool of bool | Int of int | String of string
+ type 'a T
+ val get: Proof.context -> 'a T -> 'a
+ val get_thy: theory -> 'a T -> 'a
+ val get_generic: Context.generic -> 'a T -> 'a
+ val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
+ val map_thy: 'a T -> ('a -> 'a) -> theory -> theory
+ val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
+ val put: 'a T -> 'a -> Proof.context -> Proof.context
+ val put_thy: 'a T -> 'a -> theory -> theory
+ val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
+ val print_options: Proof.context -> unit
+ val the_option: string -> value T * value
+ val bool: string -> bool -> bool T
+ val int: string -> int -> int T
+ val string: string -> string -> string T
+end;
+
+structure ConfigOption: CONFIG_OPTION =
+struct
+
+(* mixed values *)
+
+datatype value =
+ Bool of bool |
+ Int of int |
+ String of string;
+
+fun print_value (Bool true) = "true"
+ | print_value (Bool false) = "false"
+ | print_value (Int i) = signed_string_of_int i
+ | print_value (String s) = quote s;
+
+fun print_type (Bool _) = "boolean"
+ | print_type (Int _) = "integer"
+ | print_type (String _) = "string";
+
+fun same_type (Bool _) (Bool _) = true
+ | same_type (Int _) (Int _) = true
+ | same_type (String _) (String _) = true
+ | same_type _ _ = false;
+
+fun type_check f value =
+ let
+ val value' = f value;
+ val _ = same_type value value' orelse
+ error ("Ill-typed configuration option: " ^ print_type value ^
+ " expected,\nbut " ^ print_type value' ^ " was found");
+ in value' end;
+
+structure ConfigOptionData = GenericDataFun
+(
+ type T = value Inttab.table;
+ val empty = Inttab.empty;
+ val extend = I;
+ fun merge _ = Inttab.merge (K true);
+);
+
+
+(* abstract configuration options *)
+
+datatype 'a T = ConfigOption of
+ {get_value: Context.generic -> 'a,
+ map_value: ('a -> 'a) -> Context.generic -> Context.generic};
+
+fun get_generic context (ConfigOption {get_value, ...}) = get_value context;
+fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
+fun get_thy thy = get_generic (Context.Theory thy);
+
+fun map_generic (ConfigOption {map_value, ...}) f context = map_value f context;
+fun map_ctxt config f = Context.proof_map (map_generic config f);
+fun map_thy config f = Context.theory_map (map_generic config f);
+
+fun put_generic config value = map_generic config (K value);
+fun put_ctxt config value = map_ctxt config (K value);
+fun put_thy config value = map_thy config (K value);
+
+
+(* global declarations *)
+
+local val global_configs = ref (Symtab.empty: (value T * value) Symtab.table) in
+
+fun print_options ctxt =
+ let
+ fun prt (name, (config, default)) =
+ Pretty.block [Pretty.str (name ^ ": " ^ print_type default ^ " ="), Pretty.brk 1,
+ Pretty.str (print_value (get_ctxt ctxt config))];
+ val configs = sort_wrt #1 (Symtab.dest (! global_configs));
+ in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
+
+fun the_option name =
+ (case Symtab.lookup (! global_configs) name of SOME cfg => cfg
+ | NONE => error ("Unknown configuration option " ^ quote name));
+
+fun declare make dest name default =
+ let
+ val id = serial ();
+
+ val default_value = make default;
+ fun get_value context =
+ the_default default_value (Inttab.lookup (ConfigOptionData.get context) id);
+ fun map_value f = ConfigOptionData.map (Inttab.map_default (id, default_value) (type_check f));
+ val config_value = ConfigOption {get_value = get_value, map_value = map_value};
+
+ val _ = CRITICAL (fn () =>
+ (if Symtab.defined (! global_configs) name
+ then warning ("Hiding existing configuration option " ^ quote name) else ();
+ change global_configs (Symtab.update (name, (config_value, default_value)))));
+
+ in
+ ConfigOption {get_value = dest o get_value, map_value = fn f => map_value (make o f o dest)}
+ end;
+
+end;
+
+val bool = declare Bool (fn Bool b => b);
+val int = declare Int (fn Int i => i);
+val string = declare String (fn String s => s);
+
+
+(*final declarations of this structure!*)
+val get = get_ctxt;
+val map = map_ctxt;
+val put = put_ctxt;
+
+end;