clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed May 15 22:02:51 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed May 15 22:30:24 2013 +0200
@@ -37,7 +37,10 @@
val _ =
ProofGeneral.preference_bool ProofGeneral.category_tracing
- auto "auto-nitpick" "Run Nitpick automatically"
+ NONE
+ auto
+ "auto-nitpick"
+ "Run Nitpick automatically"
type raw_param = string * string list
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed May 15 22:02:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed May 15 22:30:24 2013 +0200
@@ -46,7 +46,10 @@
val _ =
ProofGeneral.preference_bool ProofGeneral.category_tracing
- auto "auto-sledgehammer" "Run Sledgehammer automatically"
+ NONE
+ auto
+ "auto-sledgehammer"
+ "Run Sledgehammer automatically"
(** Sledgehammer commands **)
@@ -66,12 +69,14 @@
val _ =
ProofGeneral.preference_string ProofGeneral.category_proof
+ NONE
provers
"Sledgehammer: Provers"
"Default automatic provers (separated by whitespace)"
val _ =
ProofGeneral.preference_int ProofGeneral.category_proof
+ NONE
timeout
"Sledgehammer: Time Limit"
"ATPs will be interrupted after this time (in seconds)"
--- a/src/HOL/Tools/try0.ML Wed May 15 22:02:51 2013 +0200
+++ b/src/HOL/Tools/try0.ML Wed May 15 22:30:24 2013 +0200
@@ -28,7 +28,10 @@
val _ =
ProofGeneral.preference_bool ProofGeneral.category_tracing
- auto "auto-try0" "Try standard proof methods"
+ NONE
+ auto
+ "auto-try0"
+ "Try standard proof methods"
val default_timeout = seconds 5.0
--- a/src/Pure/Tools/proof_general.ML Wed May 15 22:02:51 2013 +0200
+++ b/src/Pure/Tools/proof_general.ML Wed May 15 22:30:24 2013 +0200
@@ -18,13 +18,17 @@
val pgipint: pgiptype
val pgipfloat: pgiptype
val pgipstring: pgiptype
- val preference: category -> (unit -> string) -> (string -> unit) ->
- string -> string -> string -> unit
- val preference_bool: category -> bool Unsynchronized.ref -> string -> string -> unit
- val preference_int: category -> int Unsynchronized.ref -> string -> string -> unit
- val preference_real: category -> real Unsynchronized.ref -> string -> string -> unit
- val preference_string: category -> string Unsynchronized.ref -> string -> string -> unit
- val preference_option: category -> string -> string -> string -> unit
+ val preference: category -> string option ->
+ (unit -> string) -> (string -> unit) -> string -> string -> string -> unit
+ val preference_bool: category -> string option ->
+ bool Unsynchronized.ref -> string -> string -> unit
+ val preference_int: category -> string option ->
+ int Unsynchronized.ref -> string -> string -> unit
+ val preference_real: category -> string option ->
+ real Unsynchronized.ref -> string -> string -> unit
+ val preference_string: category -> string option ->
+ string Unsynchronized.ref -> string -> string -> unit
+ val preference_option: category -> string option -> string -> string -> string -> unit
structure ThyLoad: sig val add_path: string -> unit end
val thm_deps: bool Unsynchronized.ref
val proof_generalN: string
@@ -52,8 +56,8 @@
type preference =
{category: string,
+ override: string option,
descr: string,
- default: string,
pgiptype: pgiptype,
get: unit -> string,
set: string -> unit};
@@ -79,32 +83,36 @@
fun all_preferences () =
rev (Synchronized.value preferences)
- |> map (fn (name, {category, descr, default, pgiptype, ...}) =>
- (category, {name = name, descr = descr, default = default, pgiptype = pgiptype}))
+ |> map (fn (name, {category, descr, pgiptype, get, ...}) =>
+ (category, {name = name, descr = descr, default = get (), pgiptype = pgiptype}))
|> AList.group (op =);
+fun init_preferences () =
+ Synchronized.value preferences
+ |> List.app (fn (_, {set, override = SOME value, ...}) => set value | _ => ());
+
end;
(* raw preferences *)
-fun preference category get set typ name descr =
+fun preference category override get set typ name descr =
add_preference name
- {category = category, descr = descr, pgiptype = typ, get = get, set = set, default = get ()};
+ {category = category, override = override, descr = descr, pgiptype = typ, get = get, set = set};
-fun preference_ref category read write typ r =
- preference category (fn () => read (! r)) (fn x => r := write x) typ;
+fun preference_ref category override read write typ r =
+ preference category override (fn () => read (! r)) (fn x => r := write x) typ;
-fun preference_bool category = preference_ref category Markup.print_bool Markup.parse_bool pgipbool;
-fun preference_int category = preference_ref category Markup.print_int Markup.parse_int pgipint;
-fun preference_real category = preference_ref category Markup.print_real Markup.parse_real pgipfloat;
-fun preference_string category = preference_ref category I I pgipstring;
+fun preference_bool x y = preference_ref x y Markup.print_bool Markup.parse_bool pgipbool;
+fun preference_int x y = preference_ref x y Markup.print_int Markup.parse_int pgipint;
+fun preference_real x y = preference_ref x y Markup.print_real Markup.parse_real pgipfloat;
+fun preference_string x y = preference_ref x y I I pgipstring;
(* system options *)
-fun preference_option category option_name pgip_name descr =
+fun preference_option category override option_name pgip_name descr =
let
val typ = Options.default_typ option_name;
val pgiptype =
@@ -115,8 +123,8 @@
in
add_preference pgip_name
{category = category,
+ override = override,
descr = descr,
- default = Options.get_default option_name,
pgiptype = pgiptype,
get = fn () => Options.get_default option_name,
set = Options.put_default option_name}
@@ -399,6 +407,7 @@
setup_thy_loader ();
setup_present_hook ();
initialized := true);
+ init_preferences ();
sync_thy_loader ();
Unsynchronized.change print_mode (update (op =) proof_generalN);
Secure.PG_setup ();
--- a/src/Pure/Tools/proof_general_pure.ML Wed May 15 22:02:51 2013 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML Wed May 15 22:30:24 2013 +0200
@@ -9,42 +9,49 @@
val _ =
ProofGeneral.preference_bool ProofGeneral.category_display
+ NONE
Printer.show_types_default
"show-types"
"Include types in display of Isabelle terms";
val _ =
ProofGeneral.preference_bool ProofGeneral.category_display
+ NONE
Printer.show_sorts_default
"show-sorts"
"Include sorts in display of Isabelle terms";
val _ =
ProofGeneral.preference_bool ProofGeneral.category_display
+ NONE
Goal_Display.show_consts_default
"show-consts"
"Show types of consts in Isabelle goal display";
val _ =
ProofGeneral.preference_option ProofGeneral.category_display
+ NONE
@{option names_long}
"long-names"
"Show fully qualified names in Isabelle terms";
val _ =
ProofGeneral.preference_bool ProofGeneral.category_display
+ NONE
Printer.show_brackets_default
"show-brackets"
"Show full bracketing in Isabelle terms";
val _ =
ProofGeneral.preference_bool ProofGeneral.category_display
+ NONE
Goal_Display.show_main_goal_default
"show-main-goal"
"Show main goal in proof state display";
val _ =
ProofGeneral.preference_bool ProofGeneral.category_display
+ NONE
Syntax_Trans.eta_contract_default
"eta-contract"
"Print terms eta-contracted";
@@ -54,12 +61,14 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_advanced_display
+ NONE
@{option goals_limit}
"goals-limit"
"Setting for maximum number of subgoals to be printed";
val _ =
ProofGeneral.preference ProofGeneral.category_advanced_display
+ NONE
(Markup.print_int o get_print_depth)
(print_depth o Markup.parse_int)
ProofGeneral.pgipint
@@ -68,6 +77,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_advanced_display
+ NONE
@{option show_question_marks}
"show-question-marks"
"Show leading question mark of variable name";
@@ -77,36 +87,42 @@
val _ =
ProofGeneral.preference_bool ProofGeneral.category_tracing
+ NONE
Raw_Simplifier.simp_trace_default
"trace-simplifier"
"Trace simplification rules";
val _ =
ProofGeneral.preference_int ProofGeneral.category_tracing
+ NONE
Raw_Simplifier.simp_trace_depth_limit_default
"trace-simplifier-depth"
"Trace simplifier depth limit";
val _ =
ProofGeneral.preference_bool ProofGeneral.category_tracing
+ NONE
Pattern.trace_unify_fail
"trace-unification"
"Output error diagnostics during unification";
val _ =
ProofGeneral.preference_bool ProofGeneral.category_tracing
+ NONE
Toplevel.timing
"global-timing"
"Whether to enable timing in Isabelle";
val _ =
ProofGeneral.preference_bool ProofGeneral.category_tracing
+ NONE
Toplevel.debug
"debugging"
"Whether to enable debugging";
val _ =
ProofGeneral.preference_bool ProofGeneral.category_tracing
+ NONE
ProofGeneral.thm_deps
"theorem-dependencies"
"Track theorem dependencies within Proof General";
@@ -115,36 +131,38 @@
(* proof *)
val _ =
- Unsynchronized.setmp quick_and_dirty true (fn () =>
- ProofGeneral.preference_bool ProofGeneral.category_proof
- quick_and_dirty
- "quick-and-dirty"
- "Take a few short cuts") ();
+ ProofGeneral.preference_bool ProofGeneral.category_proof
+ (SOME "true")
+ quick_and_dirty
+ "quick-and-dirty"
+ "Take a few short cuts";
val _ =
ProofGeneral.preference_bool ProofGeneral.category_proof
+ NONE
Goal.skip_proofs
"skip-proofs"
"Skip over proofs";
val _ =
- Unsynchronized.setmp Proofterm.proofs 1 (fn () =>
- ProofGeneral.preference ProofGeneral.category_proof
- (Markup.print_bool o Proofterm.proofs_enabled)
- (fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 1))
- ProofGeneral.pgipbool
- "full-proofs"
- "Record full proof objects internally") ();
+ ProofGeneral.preference ProofGeneral.category_proof
+ NONE
+ (Markup.print_bool o Proofterm.proofs_enabled)
+ (fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 1))
+ ProofGeneral.pgipbool
+ "full-proofs"
+ "Record full proof objects internally";
val _ =
- Unsynchronized.setmp Multithreading.max_threads 0 (fn () =>
- ProofGeneral.preference_int ProofGeneral.category_proof
- Multithreading.max_threads
- "max-threads"
- "Maximum number of threads") ();
+ ProofGeneral.preference_int ProofGeneral.category_proof
+ NONE
+ Multithreading.max_threads
+ "max-threads"
+ "Maximum number of threads";
val _ =
ProofGeneral.preference ProofGeneral.category_proof
+ NONE
(fn () => Markup.print_bool (! Goal.parallel_proofs >= 1))
(fn s => Goal.parallel_proofs := (if Markup.parse_bool s then 1 else 0))
ProofGeneral.pgipbool
--- a/src/Tools/quickcheck.ML Wed May 15 22:02:51 2013 +0200
+++ b/src/Tools/quickcheck.ML Wed May 15 22:30:24 2013 +0200
@@ -97,11 +97,11 @@
val auto = Unsynchronized.ref false;
val _ =
- Unsynchronized.setmp auto true (fn () =>
- ProofGeneral.preference_bool ProofGeneral.category_tracing
- auto
- "auto-quickcheck"
- "Run Quickcheck automatically") ()
+ ProofGeneral.preference_bool ProofGeneral.category_tracing
+ (SOME "true")
+ auto
+ "auto-quickcheck"
+ "Run Quickcheck automatically";
(* quickcheck report *)
--- a/src/Tools/solve_direct.ML Wed May 15 22:02:51 2013 +0200
+++ b/src/Tools/solve_direct.ML Wed May 15 22:30:24 2013 +0200
@@ -37,11 +37,11 @@
val max_solutions = Unsynchronized.ref 5;
val _ =
- Unsynchronized.setmp auto true (fn () =>
- ProofGeneral.preference_bool ProofGeneral.category_tracing
- auto
- "auto-solve-direct"
- ("Run " ^ quote solve_directN ^ " automatically")) ();
+ ProofGeneral.preference_bool ProofGeneral.category_tracing
+ (SOME "true")
+ auto
+ "auto-solve-direct"
+ ("Run " ^ quote solve_directN ^ " automatically");
(* solve_direct command *)
--- a/src/Tools/try.ML Wed May 15 22:02:51 2013 +0200
+++ b/src/Tools/try.ML Wed May 15 22:30:24 2013 +0200
@@ -36,6 +36,7 @@
val _ =
ProofGeneral.preference_real ProofGeneral.category_tracing
+ NONE
auto_time_limit
"auto-try-time-limit"
"Time limit for automatically tried tools (in seconds)"