--- a/src/Doc/antiquote_setup.ML Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Doc/antiquote_setup.ML Tue Apr 08 14:59:36 2014 +0200
@@ -201,6 +201,10 @@
val _ = Context_Position.reports ctxt (map (pair pos) markup);
in true end;
+fun check_system_option ctxt (name, pos) =
+ (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true)
+ handle ERROR _ => false;
+
fun check_tool ctxt (name, pos) =
let
fun tool dir =
@@ -265,7 +269,7 @@
entity_antiqs (can o Thy_Output.check_command) "" @{binding antiquotation} #>
entity_antiqs (can o Thy_Output.check_option) "" @{binding antiquotation_option} #>
entity_antiqs no_check "isatt" @{binding setting} #>
- entity_antiqs no_check "isatt" @{binding system_option} #>
+ entity_antiqs check_system_option "isatt" @{binding system_option} #>
entity_antiqs no_check "" @{binding inference} #>
entity_antiqs no_check "isatt" @{binding executable} #>
entity_antiqs check_tool "isatool" @{binding tool} #>
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Tue Apr 08 14:59:36 2014 +0200
@@ -124,7 +124,7 @@
| SOME _ => (GenuineCex, Quickcheck.timings_of result)
end) ()
handle TimeLimit.TimeOut =>
- (Timeout, [("timelimit", Real.floor (Options.default_real @{option auto_time_limit}))])
+ (Timeout, [("timelimit", Real.floor (Options.default_real @{system_option auto_time_limit}))])
fun quickcheck_mtd change_options quickcheck_generator =
("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options)
--- a/src/HOL/Prolog/prolog.ML Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/Prolog/prolog.ML Tue Apr 08 14:59:36 2014 +0200
@@ -2,7 +2,7 @@
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
-Options.default_put_bool @{option show_main_goal} true;
+Options.default_put_bool @{system_option show_main_goal} true;
structure Prolog =
struct
--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Tue Apr 08 14:59:36 2014 +0200
@@ -285,7 +285,7 @@
type tptp_problem = tptp_line list
-fun debug f x = if Options.default_bool @{option ML_exception_trace} then (f x; ()) else ()
+fun debug f x = if Options.default_bool @{system_option ML_exception_trace} then (f x; ()) else ()
fun nameof_tff_atom_type (Atom_type str) = str
| nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Tue Apr 08 14:59:36 2014 +0200
@@ -42,7 +42,7 @@
ML {*
if test_all @{context} then ()
else
- (Options.default_put_bool @{option ML_exception_trace} true;
+ (Options.default_put_bool @{system_option ML_exception_trace} true;
default_print_depth 200; (* FIXME proper ML_print_depth within context!? *)
PolyML.Compiler.maxInlineSize := 0)
*}
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Tue Apr 08 14:59:36 2014 +0200
@@ -34,7 +34,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- @{option auto_nitpick}
+ @{system_option auto_nitpick}
"auto-nitpick"
"Run Nitpick automatically"
@@ -396,6 +396,6 @@
fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
-val _ = Try.tool_setup (nitpickN, (50, @{option auto_nitpick}, try_nitpick))
+val _ = Try.tool_setup (nitpickN, (50, @{system_option auto_nitpick}, try_nitpick))
end;
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Tue Apr 08 14:59:36 2014 +0200
@@ -100,7 +100,7 @@
fun z3_non_commercial () =
let
- val flag1 = Options.default_string @{option z3_non_commercial}
+ val flag1 = Options.default_string @{system_option z3_non_commercial}
val flag2 = getenv "Z3_NON_COMMERCIAL"
in
if accepted flag1 then Z3_Non_Commercial_Accepted
--- a/src/HOL/Tools/SMT2/smt2_systems.ML Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML Tue Apr 08 14:59:36 2014 +0200
@@ -97,7 +97,7 @@
fun z3_non_commercial () =
let
- val flag1 = Options.default_string @{option z3_non_commercial}
+ val flag1 = Options.default_string @{system_option z3_non_commercial}
val flag2 = getenv "Z3_NON_COMMERCIAL"
in
if accepted flag1 then Z3_Non_Commercial_Accepted
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue Apr 08 14:59:36 2014 +0200
@@ -43,7 +43,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- @{option auto_sledgehammer}
+ @{system_option auto_sledgehammer}
"auto-sledgehammer"
"Run Sledgehammer automatically"
@@ -72,7 +72,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_proof
NONE
- @{option sledgehammer_timeout}
+ @{system_option sledgehammer_timeout}
"Sledgehammer: Time Limit"
"ATPs will be interrupted after this time (in seconds)"
@@ -229,7 +229,7 @@
|> fold (AList.default (op =))
[("provers", [(case !provers of "" => default_provers_param_value mode ctxt | s => s)]),
("timeout",
- let val timeout = Options.default_int @{option sledgehammer_timeout} in
+ let val timeout = Options.default_int @{system_option sledgehammer_timeout} in
[if timeout <= 0 then "none" else string_of_int timeout]
end)]
end
@@ -472,7 +472,7 @@
state
end
-val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
+val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer))
val _ =
Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>
--- a/src/HOL/Tools/try0.ML Tue Apr 08 14:56:55 2014 +0200
+++ b/src/HOL/Tools/try0.ML Tue Apr 08 14:59:36 2014 +0200
@@ -25,7 +25,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- @{option auto_methods}
+ @{system_option auto_methods}
"auto-try0"
"Try standard proof methods";
@@ -193,6 +193,6 @@
fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []);
-val _ = Try.tool_setup (try0N, (30, @{option auto_methods}, try_try0));
+val _ = Try.tool_setup (try0N, (30, @{system_option auto_methods}, try_try0));
end;
--- a/src/Pure/Isar/isar_syn.ML Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Apr 08 14:59:36 2014 +0200
@@ -984,7 +984,7 @@
(opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
Toplevel.keep (fn state =>
(if Isabelle_Process.is_active () then error "Illegal TTY command" else ();
- case limit of NONE => () | SOME n => Options.default_put_int @{option goals_limit} n;
+ case limit of NONE => () | SOME n => Options.default_put_int @{system_option goals_limit} n;
Toplevel.quiet := false;
Print_Mode.with_modes modes (Toplevel.print_state true) state))));
--- a/src/Pure/ML/ml_antiquotations.ML Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Tue Apr 08 14:59:36 2014 +0200
@@ -8,17 +8,10 @@
struct
val _ = Theory.setup
- (ML_Antiquotation.value @{binding option}
+ (ML_Antiquotation.value @{binding system_option}
(Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
- let
- val def_pos =
- Options.default_position name
- handle ERROR msg => error (msg ^ Position.here pos);
- val markup =
- Markup.properties (Position.def_properties_of def_pos)
- (Markup.entity Markup.system_optionN name);
- val _ = Context_Position.report ctxt pos markup;
- in ML_Syntax.print_string name end)) #>
+ (Context_Position.report ctxt pos (Options.default_markup (name, pos));
+ ML_Syntax.print_string name))) #>
ML_Antiquotation.value @{binding theory}
(Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
--- a/src/Pure/System/options.ML Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Pure/System/options.ML Tue Apr 08 14:59:36 2014 +0200
@@ -13,7 +13,7 @@
val unknownT: string
type T
val empty: T
- val position: T -> string -> Position.T
+ val markup: T -> string * Position.T -> Markup.T
val typ: T -> string -> string
val bool: T -> string -> bool
val int: T -> string -> int
@@ -27,7 +27,7 @@
val update: string -> string -> T -> T
val decode: XML.body -> T
val default: unit -> T
- val default_position: string -> Position.T
+ val default_markup: string * Position.T -> Markup.T
val default_typ: string -> string
val default_bool: string -> bool
val default_int: string -> int
@@ -75,9 +75,19 @@
end;
-(* declaration *)
+(* markup *)
-fun position options name = #pos (check_name options name);
+fun markup options (name, pos) =
+ let
+ val opt =
+ check_name options name
+ handle ERROR msg => error (msg ^ Position.here pos);
+ val props = Position.def_properties_of (#pos opt);
+ in Markup.properties props (Markup.entity Markup.system_optionN name) end;
+
+
+(* typ *)
+
fun typ options name = #typ (check_name options name);
@@ -173,7 +183,7 @@
SOME options => options
| NONE => err_no_default ());
-fun default_position name = position (default ()) name;
+fun default_markup arg = markup (default ()) arg;
fun default_typ name = typ (default ()) name;
fun default_bool name = bool (default ()) name;
fun default_int name = int (default ()) name;
--- a/src/Pure/Tools/find_theorems.ML Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Pure/Tools/find_theorems.ML Tue Apr 08 14:59:36 2014 +0200
@@ -206,7 +206,7 @@
val goal' = Thm.transfer thy' goal;
fun limited_etac thm i =
- Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
+ Seq.take (Options.default_int @{system_option find_theorems_tac_limit}) o etac thm i;
fun try_thm thm =
if Thm.no_prems thm then rtac thm 1 goal'
else
@@ -405,7 +405,7 @@
else raw_matches;
val len = length matches;
- val lim = the_default (Options.default_int @{option find_theorems_limit}) opt_limit;
+ val lim = the_default (Options.default_int @{system_option find_theorems_limit}) opt_limit;
in (SOME len, drop (Int.max (len - lim, 0)) matches) end;
val find =
--- a/src/Pure/Tools/proof_general_pure.ML Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML Tue Apr 08 14:59:36 2014 +0200
@@ -17,49 +17,49 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_display
NONE
- @{option show_types}
+ @{system_option show_types}
"show-types"
"Include types in display of Isabelle terms";
val _ =
ProofGeneral.preference_option ProofGeneral.category_display
NONE
- @{option show_sorts}
+ @{system_option show_sorts}
"show-sorts"
"Include sorts in display of Isabelle types";
val _ =
ProofGeneral.preference_option ProofGeneral.category_display
NONE
- @{option show_consts}
+ @{system_option show_consts}
"show-consts"
"Show types of consts in Isabelle goal display";
val _ =
ProofGeneral.preference_option ProofGeneral.category_display
NONE
- @{option names_long}
+ @{system_option names_long}
"long-names"
"Show fully qualified names in Isabelle terms";
val _ =
ProofGeneral.preference_option ProofGeneral.category_display
NONE
- @{option show_brackets}
+ @{system_option show_brackets}
"show-brackets"
"Show full bracketing in Isabelle terms";
val _ =
ProofGeneral.preference_option ProofGeneral.category_display
NONE
- @{option show_main_goal}
+ @{system_option show_main_goal}
"show-main-goal"
"Show main goal in proof state display";
val _ =
ProofGeneral.preference_option ProofGeneral.category_display
NONE
- @{option eta_contract}
+ @{system_option eta_contract}
"eta-contract"
"Print terms eta-contracted";
@@ -69,7 +69,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_advanced_display
NONE
- @{option goals_limit}
+ @{system_option goals_limit}
"goals-limit"
"Setting for maximum number of subgoals to be printed";
@@ -85,7 +85,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_advanced_display
NONE
- @{option show_question_marks}
+ @{system_option show_question_marks}
"show-question-marks"
"Show leading question mark of variable name";
@@ -123,7 +123,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- @{option ML_exception_trace}
+ @{system_option ML_exception_trace}
"debugging"
"Whether to enable exception trace for toplevel command execution";
@@ -140,14 +140,14 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_proof
(SOME "true")
- @{option quick_and_dirty}
+ @{system_option quick_and_dirty}
"quick-and-dirty"
"Take a few short cuts";
val _ =
ProofGeneral.preference_option ProofGeneral.category_proof
NONE
- @{option skip_proofs}
+ @{system_option skip_proofs}
"skip-proofs"
"Skip over proofs";
--- a/src/Tools/quickcheck.ML Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Tools/quickcheck.ML Tue Apr 08 14:59:36 2014 +0200
@@ -95,7 +95,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- @{option auto_quickcheck}
+ @{system_option auto_quickcheck}
"auto-quickcheck"
"Run Quickcheck automatically";
@@ -584,7 +584,7 @@
end
|> `(fn (outcome_code, _) => outcome_code = genuineN);
-val _ = Try.tool_setup (quickcheckN, (20, @{option auto_quickcheck}, try_quickcheck));
+val _ = Try.tool_setup (quickcheckN, (20, @{system_option auto_quickcheck}, try_quickcheck));
end;
--- a/src/Tools/solve_direct.ML Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Tools/solve_direct.ML Tue Apr 08 14:59:36 2014 +0200
@@ -37,7 +37,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- @{option auto_solve_direct}
+ @{system_option auto_solve_direct}
"auto-solve-direct"
("Run " ^ quote solve_directN ^ " automatically");
@@ -115,6 +115,6 @@
fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try)
-val _ = Try.tool_setup (solve_directN, (10, @{option auto_solve_direct}, try_solve_direct));
+val _ = Try.tool_setup (solve_directN, (10, @{system_option auto_solve_direct}, try_solve_direct));
end;
--- a/src/Tools/try.ML Tue Apr 08 14:56:55 2014 +0200
+++ b/src/Tools/try.ML Tue Apr 08 14:59:36 2014 +0200
@@ -32,7 +32,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_tracing
(SOME "4.0")
- @{option auto_time_limit}
+ @{system_option auto_time_limit}
"auto-try-time-limit"
"Time limit for automatically tried tools (in seconds)"
@@ -103,7 +103,7 @@
val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
let
- val auto_time_limit = Options.default_real @{option auto_time_limit}
+ val auto_time_limit = Options.default_real @{system_option auto_time_limit}
in
if interact andalso not (!Toplevel.quiet) andalso auto_time_limit > 0.0 then
TimeLimit.timeLimit (seconds auto_time_limit) auto_try state
@@ -120,7 +120,7 @@
(fn {command_name, ...} =>
if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
SOME
- {delay = SOME (seconds (Options.default_real @{option auto_time_start})),
+ {delay = SOME (seconds (Options.default_real @{system_option auto_time_start})),
pri = ~ weight,
persistent = true,
strict = true,
@@ -128,7 +128,7 @@
let
val state = Toplevel.proof_of st
|> Proof.map_context (Context_Position.set_visible false)
- val auto_time_limit = Options.default_real @{option auto_time_limit}
+ val auto_time_limit = Options.default_real @{system_option auto_time_limit}
in
if auto_time_limit > 0.0 then
(case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of