--- a/src/Pure/General/name_space.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/General/name_space.ML Thu Jan 03 14:12:44 2019 +0100
@@ -19,11 +19,8 @@
val entry_ord: T -> string * string -> order
val is_concealed: T -> string -> bool
val intern: T -> xstring -> string
- val names_long_raw: Config.raw
val names_long: bool Config.T
- val names_short_raw: Config.raw
val names_short: bool Config.T
- val names_unique_raw: Config.raw
val names_unique: bool Config.T
val extern: Proof.context -> T -> string -> xstring
val extern_ord: Proof.context -> T -> string * string -> order
@@ -215,14 +212,9 @@
(* extern *)
-val names_long_raw = Config.declare_option ("names_long", \<^here>);
-val names_long = Config.bool names_long_raw;
-
-val names_short_raw = Config.declare_option ("names_short", \<^here>);
-val names_short = Config.bool names_short_raw;
-
-val names_unique_raw = Config.declare_option ("names_unique", \<^here>);
-val names_unique = Config.bool names_unique_raw;
+val names_long = Config.declare_option_bool ("names_long", \<^here>);
+val names_short = Config.declare_option_bool ("names_short", \<^here>);
+val names_unique = Config.declare_option_bool ("names_unique", \<^here>);
fun extern ctxt space name =
let
--- a/src/Pure/Isar/attrib.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Isar/attrib.ML Thu Jan 03 14:12:44 2019 +0100
@@ -380,7 +380,7 @@
structure Configs = Theory_Data
(
- type T = Config.raw Symtab.table;
+ type T = Config.value Config.T Symtab.table;
val empty = Symtab.empty;
val extend = I;
fun merge data = Symtab.merge (K true) data;
@@ -438,6 +438,11 @@
fun register_config config =
register (Binding.make (Config.name_of config, Config.pos_of config)) config;
+val register_config_bool = register_config o Config.bool_value;
+val register_config_int = register_config o Config.int_value;
+val register_config_real = register_config o Config.real_value;
+val register_config_string = register_config o Config.string_value;
+
val config_bool = declare Config.Bool Config.bool;
val config_int = declare Config.Int Config.int;
val config_real = declare Config.Real Config.real;
@@ -572,45 +577,45 @@
(Scan.succeed (Thm.rule_attribute [] (Local_Defs.abs_def_rule o Context.proof_of)))
"abstract over free variables of definitional theorem" #>
- register_config Goal.quick_and_dirty_raw #>
- register_config Ast.trace_raw #>
- register_config Ast.stats_raw #>
- register_config Printer.show_brackets_raw #>
- register_config Printer.show_sorts_raw #>
- register_config Printer.show_types_raw #>
- register_config Printer.show_markup_raw #>
- register_config Printer.show_structs_raw #>
- register_config Printer.show_question_marks_raw #>
- register_config Syntax.ambiguity_warning_raw #>
- register_config Syntax.ambiguity_limit_raw #>
- register_config Syntax_Trans.eta_contract_raw #>
- register_config Name_Space.names_long_raw #>
- register_config Name_Space.names_short_raw #>
- register_config Name_Space.names_unique_raw #>
- register_config ML_Print_Depth.print_depth_raw #>
- register_config ML_Env.ML_environment_raw #>
- register_config ML_Env.ML_read_global_raw #>
- register_config ML_Env.ML_write_global_raw #>
- register_config ML_Options.source_trace_raw #>
- register_config ML_Options.exception_trace_raw #>
- register_config ML_Options.exception_debugger_raw #>
- register_config ML_Options.debugger_raw #>
- register_config Proof_Context.show_abbrevs_raw #>
- register_config Goal_Display.goals_limit_raw #>
- register_config Goal_Display.show_main_goal_raw #>
- register_config Thm.show_consts_raw #>
- register_config Thm.show_hyps_raw #>
- register_config Thm.show_tags_raw #>
- register_config Pattern.unify_trace_failure_raw #>
- register_config Unify.trace_bound_raw #>
- register_config Unify.search_bound_raw #>
- register_config Unify.trace_simp_raw #>
- register_config Unify.trace_types_raw #>
- register_config Raw_Simplifier.simp_depth_limit_raw #>
- register_config Raw_Simplifier.simp_trace_depth_limit_raw #>
- register_config Raw_Simplifier.simp_debug_raw #>
- register_config Raw_Simplifier.simp_trace_raw #>
- register_config Local_Defs.unfold_abs_def_raw);
+ register_config_bool Goal.quick_and_dirty #>
+ register_config_bool Ast.trace #>
+ register_config_bool Ast.stats #>
+ register_config_bool Printer.show_brackets #>
+ register_config_bool Printer.show_sorts #>
+ register_config_bool Printer.show_types #>
+ register_config_bool Printer.show_markup #>
+ register_config_bool Printer.show_structs #>
+ register_config_bool Printer.show_question_marks #>
+ register_config_bool Syntax.ambiguity_warning #>
+ register_config_int Syntax.ambiguity_limit #>
+ register_config_bool Syntax_Trans.eta_contract #>
+ register_config_bool Name_Space.names_long #>
+ register_config_bool Name_Space.names_short #>
+ register_config_bool Name_Space.names_unique #>
+ register_config_int ML_Print_Depth.print_depth #>
+ register_config_string ML_Env.ML_environment #>
+ register_config_bool ML_Env.ML_read_global #>
+ register_config_bool ML_Env.ML_write_global #>
+ register_config_bool ML_Options.source_trace #>
+ register_config_bool ML_Options.exception_trace #>
+ register_config_bool ML_Options.exception_debugger #>
+ register_config_bool ML_Options.debugger #>
+ register_config_bool Proof_Context.show_abbrevs #>
+ register_config_int Goal_Display.goals_limit #>
+ register_config_bool Goal_Display.show_main_goal #>
+ register_config_bool Thm.show_consts #>
+ register_config_bool Thm.show_hyps #>
+ register_config_bool Thm.show_tags #>
+ register_config_bool Pattern.unify_trace_failure #>
+ register_config_int Unify.trace_bound #>
+ register_config_int Unify.search_bound #>
+ register_config_bool Unify.trace_simp #>
+ register_config_bool Unify.trace_types #>
+ register_config_int Raw_Simplifier.simp_depth_limit #>
+ register_config_int Raw_Simplifier.simp_trace_depth_limit #>
+ register_config_bool Raw_Simplifier.simp_debug #>
+ register_config_bool Raw_Simplifier.simp_trace #>
+ register_config_bool Local_Defs.unfold_abs_def);
(* internal source *)
--- a/src/Pure/Isar/local_defs.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Isar/local_defs.ML Thu Jan 03 14:12:44 2019 +0100
@@ -23,7 +23,6 @@
val meta_rewrite_conv: Proof.context -> conv
val meta_rewrite_rule: Proof.context -> thm -> thm
val abs_def_rule: Proof.context -> thm -> thm
- val unfold_abs_def_raw: Config.raw
val unfold_abs_def: bool Config.T
val unfold: Proof.context -> thm list -> thm -> thm
val unfold_goals: Proof.context -> thm list -> thm -> thm
@@ -207,8 +206,7 @@
(* unfold object-level rules *)
-val unfold_abs_def_raw = Config.declare ("unfold_abs_def", \<^here>) (K (Config.Bool true));
-val unfold_abs_def = Config.bool unfold_abs_def_raw;
+val unfold_abs_def = Config.declare_bool ("unfold_abs_def", \<^here>) (K true);
local
--- a/src/Pure/Isar/method.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Isar/method.ML Thu Jan 03 14:12:44 2019 +0100
@@ -495,7 +495,7 @@
val _ = Seq.pull (method ctxt' src' ctxt' [] (ctxt', Goal.protect 0 Drule.dummy_thm));
in map Token.closure src' end;
-val closure = Config.bool (Config.declare ("Method.closure", \<^here>) (K (Config.Bool true)));
+val closure = Config.declare_bool ("Method.closure", \<^here>) (K true);
fun method_cmd ctxt =
check_src ctxt #>
@@ -605,8 +605,7 @@
(* sections *)
-val old_section_parser =
- Config.bool (Config.declare ("Method.old_section_parser", \<^here>) (K (Config.Bool false)));
+val old_section_parser = Config.declare_bool ("Method.old_section_parser", \<^here>) (K false);
local
--- a/src/Pure/Isar/outer_syntax.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Thu Jan 03 14:12:44 2019 +0100
@@ -174,8 +174,7 @@
(* parse commands *)
-val bootstrap =
- Config.bool (Config.declare ("Outer_Syntax.bootstrap", \<^here>) (K (Config.Bool true)));
+val bootstrap = Config.declare_bool ("Outer_Syntax.bootstrap", \<^here>) (K true);
local
--- a/src/Pure/Isar/proof_context.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Isar/proof_context.ML Thu Jan 03 14:12:44 2019 +0100
@@ -93,7 +93,6 @@
val read_term_pattern: Proof.context -> string -> term
val read_term_schematic: Proof.context -> string -> term
val read_term_abbrev: Proof.context -> string -> term
- val show_abbrevs_raw: Config.raw
val show_abbrevs: bool Config.T
val expand_abbrevs: Proof.context -> term -> term
val cert_term: Proof.context -> term -> term
@@ -633,8 +632,7 @@
end;
-val show_abbrevs_raw = Config.declare ("show_abbrevs", \<^here>) (fn _ => Config.Bool true);
-val show_abbrevs = Config.bool show_abbrevs_raw;
+val show_abbrevs = Config.declare_bool ("show_abbrevs", \<^here>) (K true);
fun contract_abbrevs ctxt t =
let
@@ -666,8 +664,7 @@
local
-val dummies =
- Config.bool (Config.declare ("Proof_Context.dummies", \<^here>) (K (Config.Bool false)));
+val dummies = Config.declare_bool ("Proof_Context.dummies", \<^here>) (K false);
fun check_dummies ctxt t =
if Config.get ctxt dummies then t
@@ -978,8 +975,7 @@
(* retrieve facts *)
-val dynamic_facts_dummy =
- Config.bool (Config.declare ("dynamic_facts_dummy_", \<^here>) (fn _ => Config.Bool false));
+val dynamic_facts_dummy = Config.declare_bool ("dynamic_facts_dummy_", \<^here>) (K false);
local
@@ -1048,9 +1044,7 @@
(* inner statement mode *)
-val inner_stmt =
- Config.bool (Config.declare ("inner_stmt", \<^here>) (K (Config.Bool false)));
-
+val inner_stmt = Config.declare_bool ("inner_stmt", \<^here>) (K false);
fun is_stmt ctxt = Config.get ctxt inner_stmt;
val set_stmt = Config.put inner_stmt;
val restore_stmt = set_stmt o is_stmt;
@@ -1569,11 +1563,8 @@
(* core context *)
-val debug =
- Config.bool (Config.declare ("Proof_Context.debug", \<^here>) (K (Config.Bool false)));
-
-val verbose =
- Config.bool (Config.declare ("Proof_Context.verbose", \<^here>) (K (Config.Bool false)));
+val debug = Config.declare_bool ("Proof_Context.debug", \<^here>) (K false);
+val verbose = Config.declare_bool ("Proof_Context.verbose", \<^here>) (K false);
fun pretty_ctxt ctxt =
if not (Config.get ctxt debug) then []
--- a/src/Pure/ML/ml_env.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/ML/ml_env.ML Thu Jan 03 14:12:44 2019 +0100
@@ -9,11 +9,8 @@
sig
val Isabelle: string
val SML: string
- val ML_environment_raw: Config.raw
val ML_environment: string Config.T
- val ML_read_global_raw: Config.raw
val ML_read_global: bool Config.T
- val ML_write_global_raw: Config.raw
val ML_write_global: bool Config.T
val inherit: Context.generic list -> Context.generic -> Context.generic
type operations =
@@ -48,17 +45,13 @@
val Isabelle = "Isabelle";
val SML = "SML";
-val ML_environment_raw = Config.declare ("ML_environment", \<^here>) (fn _ => Config.String Isabelle);
-val ML_environment = Config.string ML_environment_raw;
+val ML_environment = Config.declare_string ("ML_environment", \<^here>) (K Isabelle);
(* global read/write *)
-val ML_read_global_raw = Config.declare ("ML_read_global", \<^here>) (fn _ => Config.Bool true);
-val ML_write_global_raw = Config.declare ("ML_write_global", \<^here>) (fn _ => Config.Bool true);
-
-val ML_read_global = Config.bool ML_read_global_raw;
-val ML_write_global = Config.bool ML_write_global_raw;
+val ML_read_global = Config.declare_bool ("ML_read_global", \<^here>) (K true);
+val ML_write_global = Config.declare_bool ("ML_write_global", \<^here>) (K true);
fun read_global context = Config.get_generic context ML_read_global;
fun write_global context = Config.get_generic context ML_write_global;
--- a/src/Pure/ML/ml_options.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/ML/ml_options.ML Thu Jan 03 14:12:44 2019 +0100
@@ -6,15 +6,11 @@
signature ML_OPTIONS =
sig
- val source_trace_raw: Config.raw
val source_trace: bool Config.T
- val exception_trace_raw: Config.raw
val exception_trace: bool Config.T
val exception_trace_enabled: Context.generic option -> bool
- val exception_debugger_raw: Config.raw
val exception_debugger: bool Config.T
val exception_debugger_enabled: Context.generic option -> bool
- val debugger_raw: Config.raw
val debugger: bool Config.T
val debugger_enabled: Context.generic option -> bool
end;
@@ -24,38 +20,33 @@
(* source trace *)
-val source_trace_raw =
- Config.declare ("ML_source_trace", \<^here>) (fn _ => Config.Bool false);
-val source_trace = Config.bool source_trace_raw;
+val source_trace = Config.declare_bool ("ML_source_trace", \<^here>) (K false);
(* exception trace *)
-val exception_trace_raw = Config.declare_option ("ML_exception_trace", \<^here>);
-val exception_trace = Config.bool exception_trace_raw;
+val exception_trace = Config.declare_option_bool ("ML_exception_trace", \<^here>);
fun exception_trace_enabled NONE =
- (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false)
+ (Options.default_bool (Config.name_of exception_trace) handle ERROR _ => false)
| exception_trace_enabled (SOME context) = Config.get_generic context exception_trace;
(* exception debugger *)
-val exception_debugger_raw = Config.declare_option ("ML_exception_debugger", \<^here>);
-val exception_debugger = Config.bool exception_debugger_raw;
+val exception_debugger = Config.declare_option_bool ("ML_exception_debugger", \<^here>);
fun exception_debugger_enabled NONE =
- (Options.default_bool (Config.name_of exception_debugger_raw) handle ERROR _ => false)
+ (Options.default_bool (Config.name_of exception_debugger) handle ERROR _ => false)
| exception_debugger_enabled (SOME context) = Config.get_generic context exception_debugger;
(* debugger *)
-val debugger_raw = Config.declare_option ("ML_debugger", \<^here>);
-val debugger = Config.bool debugger_raw;
+val debugger = Config.declare_option_bool ("ML_debugger", \<^here>);
fun debugger_enabled NONE =
- (Options.default_bool (Config.name_of debugger_raw) handle ERROR _ => false)
+ (Options.default_bool (Config.name_of debugger) handle ERROR _ => false)
| debugger_enabled (SOME context) = Config.get_generic context debugger;
end;
--- a/src/Pure/ML/ml_print_depth.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/ML/ml_print_depth.ML Thu Jan 03 14:12:44 2019 +0100
@@ -7,7 +7,6 @@
signature ML_PRINT_DEPTH =
sig
val set_print_depth: int -> unit
- val print_depth_raw: Config.raw
val print_depth: int Config.T
val get_print_depth: unit -> int
end;
@@ -17,11 +16,8 @@
val set_print_depth = ML_Print_Depth.set_print_depth;
-val print_depth_raw =
- Config.declare ("ML_print_depth", \<^here>)
- (fn _ => Config.Int (ML_Print_Depth.get_print_depth ()));
-
-val print_depth = Config.int print_depth_raw;
+val print_depth =
+ Config.declare_int ("ML_print_depth", \<^here>) (fn _ => ML_Print_Depth.get_print_depth ());
fun get_print_depth () =
(case Context.get_generic_context () of
--- a/src/Pure/Proof/reconstruct.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Proof/reconstruct.ML Thu Jan 03 14:12:44 2019 +0100
@@ -19,8 +19,7 @@
structure Reconstruct : RECONSTRUCT =
struct
-val quiet_mode =
- Config.bool (Config.declare ("Reconstruct.quiet_mode", \<^here>) (K (Config.Bool true)));
+val quiet_mode = Config.declare_bool ("Reconstruct.quiet_mode", \<^here>) (K true);
fun message ctxt msg =
if Config.get ctxt quiet_mode then () else writeln (msg ());
--- a/src/Pure/Syntax/ast.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Syntax/ast.ML Thu Jan 03 14:12:44 2019 +0100
@@ -21,9 +21,7 @@
val fold_ast_p: string -> ast list * ast -> ast
val unfold_ast: string -> ast -> ast list
val unfold_ast_p: string -> ast -> ast list * ast
- val trace_raw: Config.raw
val trace: bool Config.T
- val stats_raw: Config.raw
val stats: bool Config.T
val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast
end;
@@ -166,11 +164,8 @@
(* normalize *)
-val trace_raw = Config.declare ("syntax_ast_trace", \<^here>) (fn _ => Config.Bool false);
-val trace = Config.bool trace_raw;
-
-val stats_raw = Config.declare ("syntax_ast_stats", \<^here>) (fn _ => Config.Bool false);
-val stats = Config.bool stats_raw;
+val trace = Config.declare_bool ("syntax_ast_trace", \<^here>) (K false);
+val stats = Config.declare_bool ("syntax_ast_stats", \<^here>) (K false);
fun message head body =
Pretty.string_of (Pretty.block [Pretty.str head, Pretty.brk 1, body]);
--- a/src/Pure/Syntax/parser.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Syntax/parser.ML Thu Jan 03 14:12:44 2019 +0100
@@ -597,8 +597,7 @@
(*trigger value for warnings*)
-val branching_level =
- Config.int (Config.declare ("syntax_branching_level", \<^here>) (fn _ => Config.Int 600));
+val branching_level = Config.declare_int ("syntax_branching_level", \<^here>) (K 600);
(*get all productions of a NT and NTs chained to it which can
be started by specified token*)
--- a/src/Pure/Syntax/printer.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Syntax/printer.ML Thu Jan 03 14:12:44 2019 +0100
@@ -18,13 +18,7 @@
signature PRINTER =
sig
include BASIC_PRINTER
- val show_brackets_raw: Config.raw
- val show_types_raw: Config.raw
- val show_sorts_raw: Config.raw
val show_markup_default: bool Unsynchronized.ref
- val show_markup_raw: Config.raw
- val show_structs_raw: Config.raw
- val show_question_marks_raw: Config.raw
val show_type_emphasis: bool Config.T
val type_emphasis: Proof.context -> typ -> bool
type prtabs
@@ -52,29 +46,14 @@
(** options for printing **)
-val show_brackets_raw = Config.declare_option ("show_brackets", \<^here>);
-val show_brackets = Config.bool show_brackets_raw;
-
-val show_types_raw = Config.declare_option ("show_types", \<^here>);
-val show_types = Config.bool show_types_raw;
-
-val show_sorts_raw = Config.declare_option ("show_sorts", \<^here>);
-val show_sorts = Config.bool show_sorts_raw;
-
+val show_brackets = Config.declare_option_bool ("show_brackets", \<^here>);
+val show_types = Config.declare_option_bool ("show_types", \<^here>);
+val show_sorts = Config.declare_option_bool ("show_sorts", \<^here>);
val show_markup_default = Unsynchronized.ref false;
-val show_markup_raw =
- Config.declare ("show_markup", \<^here>) (fn _ => Config.Bool (! show_markup_default));
-val show_markup = Config.bool show_markup_raw;
-
-val show_structs_raw =
- Config.declare ("show_structs", \<^here>) (fn _ => Config.Bool false);
-val show_structs = Config.bool show_structs_raw;
-
-val show_question_marks_raw = Config.declare_option ("show_question_marks", \<^here>);
-val show_question_marks = Config.bool show_question_marks_raw;
-
-val show_type_emphasis =
- Config.bool (Config.declare ("show_type_emphasis", \<^here>) (fn _ => Config.Bool true));
+val show_markup = Config.declare_bool ("show_markup", \<^here>) (fn _ => ! show_markup_default);
+val show_structs = Config.declare_bool ("show_structs", \<^here>) (K false);
+val show_question_marks = Config.declare_option_bool ("show_question_marks", \<^here>);
+val show_type_emphasis = Config.declare_bool ("show_type_emphasis", \<^here>) (K true);
fun type_emphasis ctxt T =
T <> dummyT andalso
@@ -223,8 +202,7 @@
| is_chain [Arg _] = true
| is_chain _ = false;
-val pretty_priority =
- Config.int (Config.declare ("Syntax.pretty_priority", \<^here>) (K (Config.Int 0)));
+val pretty_priority = Config.declare_int ("Syntax.pretty_priority", \<^here>) (K 0);
fun pretty type_mode curried ctxt tabs trf markup_trans markup_extern ast0 =
let
--- a/src/Pure/Syntax/syntax.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Syntax/syntax.ML Thu Jan 03 14:12:44 2019 +0100
@@ -10,9 +10,7 @@
type operations
val install_operations: operations -> theory -> theory
val root: string Config.T
- val ambiguity_warning_raw: Config.raw
val ambiguity_warning: bool Config.T
- val ambiguity_limit_raw: Config.raw
val ambiguity_limit: int Config.T
val encode_input: Input.source -> XML.tree
val implode_input: Input.source -> string
@@ -161,15 +159,9 @@
(* configuration options *)
-val root = Config.string (Config.declare ("syntax_root", \<^here>) (K (Config.String "any")));
-
-val ambiguity_warning_raw =
- Config.declare ("syntax_ambiguity_warning", \<^here>) (fn _ => Config.Bool true);
-val ambiguity_warning = Config.bool ambiguity_warning_raw;
-
-val ambiguity_limit_raw =
- Config.declare ("syntax_ambiguity_limit", \<^here>) (fn _ => Config.Int 10);
-val ambiguity_limit = Config.int ambiguity_limit_raw;
+val root = Config.declare_string ("syntax_root", \<^here>) (K "any");
+val ambiguity_warning = Config.declare_bool ("syntax_ambiguity_warning", \<^here>) (K true);
+val ambiguity_limit = Config.declare_int ("syntax_ambiguity_limit", \<^here>) (K 10);
(* formal input *)
@@ -330,8 +322,7 @@
(* global pretty printing *)
-val pretty_global =
- Config.bool (Config.declare ("Syntax.pretty_global", \<^here>) (K (Config.Bool false)));
+val pretty_global = Config.declare_bool ("Syntax.pretty_global", \<^here>) (K false);
fun is_pretty_global ctxt = Config.get ctxt pretty_global;
val set_pretty_global = Config.put pretty_global;
val init_pretty_global = set_pretty_global true o Proof_Context.init_global;
--- a/src/Pure/Syntax/syntax_trans.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML Thu Jan 03 14:12:44 2019 +0100
@@ -29,7 +29,6 @@
val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
- val eta_contract_raw: Config.raw
val mark_bound_abs: string * typ -> term
val mark_bound_body: string * typ -> term
val bound_vars: (string * typ) list -> term -> term
@@ -297,8 +296,7 @@
| t' => Abs (a, T, t'))
| eta_abs t = t;
-val eta_contract_raw = Config.declare_option ("eta_contract", \<^here>);
-val eta_contract = Config.bool eta_contract_raw;
+val eta_contract = Config.declare_option_bool ("eta_contract", \<^here>);
fun eta_contr ctxt tm =
if Config.get ctxt eta_contract then eta_abs tm else tm;
--- a/src/Pure/config.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/config.ML Thu Jan 03 14:12:44 2019 +0100
@@ -10,11 +10,8 @@
val print_value: value -> string
val print_type: value -> string
type 'a T
- type raw = value T
- val bool: raw -> bool T
- val int: raw -> int T
- val real: raw -> real T
- val string: raw -> string T
+ val name_of: 'a T -> string
+ val pos_of: 'a T -> Position.T
val get: Proof.context -> 'a T -> 'a
val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
val put: 'a T -> 'a -> Proof.context -> Proof.context
@@ -27,10 +24,24 @@
val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
val restore_generic: 'a T -> Context.generic -> Context.generic -> Context.generic
- val declare: string * Position.T -> (Context.generic -> value) -> raw
- val declare_option: string * Position.T -> raw
- val name_of: 'a T -> string
- val pos_of: 'a T -> Position.T
+ val bool: value T -> bool T
+ val bool_value: bool T -> value T
+ val int: value T -> int T
+ val int_value: int T -> value T
+ val real: value T -> real T
+ val real_value: real T -> value T
+ val string: value T -> string T
+ val string_value: string T -> value T
+ val declare: string * Position.T -> (Context.generic -> value) -> value T
+ val declare_bool: string * Position.T -> (Context.generic -> bool) -> bool T
+ val declare_int: string * Position.T -> (Context.generic -> int) -> int T
+ val declare_real: string * Position.T -> (Context.generic -> real) -> real T
+ val declare_string: string * Position.T -> (Context.generic -> string) -> string T
+ val declare_option: string * Position.T -> value T
+ val declare_option_bool: string * Position.T -> bool T
+ val declare_option_int: string * Position.T -> int T
+ val declare_option_real: string * Position.T -> real T
+ val declare_option_string: string * Position.T -> string T
end;
structure Config: CONFIG =
@@ -78,18 +89,8 @@
get_value: Context.generic -> 'a,
map_value: ('a -> 'a) -> Context.generic -> Context.generic};
-type raw = value T;
-
-fun coerce make dest (Config {name, pos, get_value, map_value}) = Config
- {name = name,
- pos = pos,
- get_value = dest o get_value,
- map_value = fn f => map_value (make o f o dest)};
-
-val bool = coerce Bool (fn Bool b => b);
-val int = coerce Int (fn Int i => i);
-val real = coerce Real (fn Real x => x);
-val string = coerce String (fn String s => s);
+fun name_of (Config {name, ...}) = name;
+fun pos_of (Config {pos, ...}) = pos;
fun get_generic context (Config {get_value, ...}) = get_value context;
fun map_generic (Config {map_value, ...}) f context = map_value f context;
@@ -107,7 +108,23 @@
fun restore_global config thy = put_global config (get_global thy config);
-(* context information *)
+(* coerce type *)
+
+fun coerce make dest (Config {name, pos, get_value, map_value}) = Config
+ {name = name,
+ pos = pos,
+ get_value = dest o get_value,
+ map_value = fn f => map_value (make o f o dest)};
+
+fun coerce_pair make dest = (coerce make dest, coerce dest make);
+
+val (bool, bool_value) = coerce_pair Bool (fn Bool b => b);
+val (int, int_value) = coerce_pair Int (fn Int i => i);
+val (real, real_value) = coerce_pair Real (fn Real x => x);
+val (string, string_value) = coerce_pair String (fn String s => s);
+
+
+(* context data *)
structure Data = Generic_Data
(
@@ -132,6 +149,14 @@
Config {name = name, pos = pos, get_value = get_value, map_value = map_value}
end;
+fun declare_bool name default = bool (declare name (Bool o default));
+fun declare_int name default = int (declare name (Int o default));
+fun declare_real name default = real (declare name (Real o default));
+fun declare_string name default = string (declare name (String o default));
+
+
+(* system options *)
+
fun declare_option (name, pos) =
let
val typ = Options.default_typ name;
@@ -143,9 +168,10 @@
else error ("Unknown type for option " ^ quote name ^ Position.here pos ^ " : " ^ quote typ);
in declare (name, pos) default end;
-fun name_of (Config {name, ...}) = name;
-fun pos_of (Config {pos, ...}) = pos;
-
+val declare_option_bool = bool o declare_option;
+val declare_option_int = int o declare_option;
+val declare_option_real = real o declare_option;
+val declare_option_string = string o declare_option;
(*final declarations of this structure!*)
val get = get_ctxt;
--- a/src/Pure/goal.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/goal.ML Thu Jan 03 14:12:44 2019 +0100
@@ -36,7 +36,6 @@
({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove_global: theory -> string list -> term list -> term ->
({prems: thm list, context: Proof.context} -> tactic) -> thm
- val quick_and_dirty_raw: Config.raw
val prove_sorry: Proof.context -> string list -> term list -> term ->
({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove_sorry_global: theory -> string list -> term list -> term ->
@@ -242,8 +241,7 @@
(* skip proofs *)
-val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", \<^here>);
-val quick_and_dirty = Config.bool quick_and_dirty_raw;
+val quick_and_dirty = Config.declare_option_bool ("quick_and_dirty", \<^here>);
fun prove_sorry ctxt xs asms prop tac =
if Config.get ctxt quick_and_dirty then
--- a/src/Pure/goal_display.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/goal_display.ML Thu Jan 03 14:12:44 2019 +0100
@@ -7,9 +7,7 @@
signature GOAL_DISPLAY =
sig
- val goals_limit_raw: Config.raw
val goals_limit: int Config.T
- val show_main_goal_raw: Config.raw
val show_main_goal: bool Config.T
val pretty_goals: Proof.context -> thm -> Pretty.T list
val pretty_goal: Proof.context -> thm -> Pretty.T
@@ -19,11 +17,8 @@
structure Goal_Display: GOAL_DISPLAY =
struct
-val goals_limit_raw = Config.declare_option ("goals_limit", \<^here>);
-val goals_limit = Config.int goals_limit_raw;
-
-val show_main_goal_raw = Config.declare_option ("show_main_goal", \<^here>);
-val show_main_goal = Config.bool show_main_goal_raw;
+val goals_limit = Config.declare_option_int ("goals_limit", \<^here>);
+val show_main_goal = Config.declare_option_bool ("show_main_goal", \<^here>);
(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
--- a/src/Pure/more_thm.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/more_thm.ML Thu Jan 03 14:12:44 2019 +0100
@@ -115,11 +115,8 @@
val kind: string -> attribute
val register_proofs: thm list lazy -> theory -> theory
val consolidate_theory: theory -> unit
- val show_consts_raw: Config.raw
val show_consts: bool Config.T
- val show_hyps_raw: Config.raw
val show_hyps: bool Config.T
- val show_tags_raw: Config.raw
val show_tags: bool Config.T
val pretty_flexpair: Proof.context -> term * term -> Pretty.T
val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T
@@ -686,14 +683,9 @@
(* options *)
-val show_consts_raw = Config.declare_option ("show_consts", \<^here>);
-val show_consts = Config.bool show_consts_raw;
-
-val show_hyps_raw = Config.declare ("show_hyps", \<^here>) (fn _ => Config.Bool false);
-val show_hyps = Config.bool show_hyps_raw;
-
-val show_tags_raw = Config.declare ("show_tags", \<^here>) (fn _ => Config.Bool false);
-val show_tags = Config.bool show_tags_raw;
+val show_consts = Config.declare_option_bool ("show_consts", \<^here>);
+val show_hyps = Config.declare_bool ("show_hyps", \<^here>) (K false);
+val show_tags = Config.declare_bool ("show_tags", \<^here>) (K false);
(* pretty_thm etc. *)
--- a/src/Pure/pattern.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/pattern.ML Thu Jan 03 14:12:44 2019 +0100
@@ -14,7 +14,6 @@
sig
exception Unif
exception Pattern
- val unify_trace_failure_raw: Config.raw
val unify_trace_failure: bool Config.T
val unify_types: Context.generic -> typ * typ -> Envir.env -> Envir.env
val unify: Context.generic -> term * term -> Envir.env -> Envir.env
@@ -30,9 +29,7 @@
exception Unif;
exception Pattern;
-val unify_trace_failure_raw =
- Config.declare ("unify_trace_failure", \<^here>) (fn _ => Config.Bool false);
-val unify_trace_failure = Config.bool unify_trace_failure_raw;
+val unify_trace_failure = Config.declare_bool ("unify_trace_failure", \<^here>) (K false);
fun string_of_term ctxt env binders t =
Syntax.string_of_term ctxt (Envir.norm_term env (subst_bounds (map Free binders, t)));
--- a/src/Pure/raw_simplifier.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/raw_simplifier.ML Thu Jan 03 14:12:44 2019 +0100
@@ -104,11 +104,7 @@
val set_term_ord: (term * term -> order) -> Proof.context -> Proof.context
val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
val solver: Proof.context -> solver -> int -> tactic
- val simp_depth_limit_raw: Config.raw
val default_mk_sym: Proof.context -> thm -> thm option
- val simp_trace_depth_limit_raw: Config.raw
- val simp_trace_raw: Config.raw
- val simp_debug_raw: Config.raw
val add_prems: thm list -> Proof.context -> Proof.context
val set_reorient: (Proof.context -> term list -> term -> term -> bool) ->
Proof.context -> Proof.context
@@ -396,12 +392,8 @@
As of 2017, 25 would suffice; 40 builds in a safety margin.
*)
-val simp_depth_limit_raw = Config.declare ("simp_depth_limit", \<^here>) (K (Config.Int 40));
-val simp_depth_limit = Config.int simp_depth_limit_raw;
-
-val simp_trace_depth_limit_raw =
- Config.declare ("simp_trace_depth_limit", \<^here>) (fn _ => Config.Int 1);
-val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw;
+val simp_depth_limit = Config.declare_int ("simp_depth_limit", \<^here>) (K 40);
+val simp_trace_depth_limit = Config.declare_int ("simp_trace_depth_limit", \<^here>) (K 1);
fun inc_simp_depth ctxt =
ctxt |> map_simpset1 (fn (rules, prems, (depth, exceeded)) =>
@@ -419,11 +411,8 @@
exception SIMPLIFIER of string * thm list;
-val simp_debug_raw = Config.declare ("simp_debug", \<^here>) (K (Config.Bool false));
-val simp_debug = Config.bool simp_debug_raw;
-
-val simp_trace_raw = Config.declare ("simp_trace", \<^here>) (fn _ => Config.Bool false);
-val simp_trace = Config.bool simp_trace_raw;
+val simp_debug = Config.declare_bool ("simp_debug", \<^here>) (K false);
+val simp_trace = Config.declare_bool ("simp_trace", \<^here>) (K false);
fun cond_warning ctxt msg =
if Context_Position.is_really_visible ctxt then warning (msg ()) else ();
--- a/src/Pure/type_infer.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/type_infer.ML Thu Jan 03 14:12:44 2019 +0100
@@ -100,8 +100,7 @@
(* fixate -- introduce fresh type variables *)
-val object_logic =
- Config.bool (Config.declare ("Type_Infer.object_logic", \<^here>) (K (Config.Bool true)));
+val object_logic = Config.declare_bool ("Type_Infer.object_logic", \<^here>) (K true);
fun fixate ctxt pattern ts =
let
--- a/src/Pure/type_infer_context.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/type_infer_context.ML Thu Jan 03 14:12:44 2019 +0100
@@ -20,8 +20,7 @@
(* constraints *)
-val const_sorts =
- Config.bool (Config.declare ("const_sorts", \<^here>) (K (Config.Bool true)));
+val const_sorts = Config.declare_bool ("const_sorts", \<^here>) (K true);
fun const_type ctxt =
try ((not (Config.get ctxt const_sorts) ? Type.strip_sorts) o
--- a/src/Pure/unify.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/unify.ML Thu Jan 03 14:12:44 2019 +0100
@@ -11,13 +11,9 @@
signature UNIFY =
sig
- val trace_bound_raw: Config.raw
val trace_bound: int Config.T
- val search_bound_raw: Config.raw
val search_bound: int Config.T
- val trace_simp_raw: Config.raw
val trace_simp: bool Config.T
- val trace_types_raw: Config.raw
val trace_types: bool Config.T
val hounifiers: Context.generic * Envir.env * ((term * term) list) ->
(Envir.env * (term * term) list) Seq.seq
@@ -32,20 +28,16 @@
(*Unification options*)
(*tracing starts above this depth, 0 for full*)
-val trace_bound_raw = Config.declare ("unify_trace_bound", \<^here>) (K (Config.Int 50));
-val trace_bound = Config.int trace_bound_raw;
+val trace_bound = Config.declare_int ("unify_trace_bound", \<^here>) (K 50);
(*unification quits above this depth*)
-val search_bound_raw = Config.declare ("unify_search_bound", \<^here>) (K (Config.Int 60));
-val search_bound = Config.int search_bound_raw;
+val search_bound = Config.declare_int ("unify_search_bound", \<^here>) (K 60);
(*print dpairs before calling SIMPL*)
-val trace_simp_raw = Config.declare ("unify_trace_simp", \<^here>) (K (Config.Bool false));
-val trace_simp = Config.bool trace_simp_raw;
+val trace_simp = Config.declare_bool ("unify_trace_simp", \<^here>) (K false);
(*announce potential incompleteness of type unification*)
-val trace_types_raw = Config.declare ("unify_trace_types", \<^here>) (K (Config.Bool false));
-val trace_types = Config.bool trace_types_raw;
+val trace_types = Config.declare_bool ("unify_trace_types", \<^here>) (K false);
type binderlist = (string * typ) list;
--- a/src/Pure/variable.ML Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/variable.ML Thu Jan 03 14:12:44 2019 +0100
@@ -334,9 +334,7 @@
(* inner body mode *)
-val inner_body =
- Config.bool (Config.declare ("inner_body", \<^here>) (K (Config.Bool false)));
-
+val inner_body = Config.declare_bool ("inner_body", \<^here>) (K false);
fun is_body ctxt = Config.get ctxt inner_body;
val set_body = Config.put inner_body;
fun restore_body ctxt = set_body (is_body ctxt);
@@ -344,9 +342,7 @@
(* proper mode *)
-val proper_fixes =
- Config.bool (Config.declare ("proper_fixes", \<^here>) (K (Config.Bool true)));
-
+val proper_fixes = Config.declare_bool ("proper_fixes", \<^here>) (K true);
val improper_fixes = Config.put proper_fixes false;
fun restore_proper_fixes ctxt = Config.put proper_fixes (Config.get ctxt proper_fixes);
@@ -644,9 +640,7 @@
(* focus on outermost parameters: \<And>x y z. B *)
-val bound_focus =
- Config.bool (Config.declare ("bound_focus", \<^here>) (K (Config.Bool false)));
-
+val bound_focus = Config.declare_bool ("bound_focus", \<^here>) (K false);
fun is_bound_focus ctxt = Config.get ctxt bound_focus;
val set_bound_focus = Config.put bound_focus;
fun restore_bound_focus ctxt = set_bound_focus (is_bound_focus ctxt);