sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
back to Normal mode: with output_result it is sufficient to determine TTY vs. PIDE operation;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Aug 17 14:13:18 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Aug 17 19:13:28 2013 +0200
@@ -502,9 +502,8 @@
let
val [provers_arg, timeout_arg, isar_proofs_arg] = args;
val ctxt = Proof.context_of state
- val mode = Normal_Result
- val {debug, verbose, overlord, isar_proofs, ...} = get_params mode ctxt []
+ val {debug, verbose, overlord, isar_proofs, ...} = get_params Normal ctxt []
val override_params =
([("timeout", [timeout_arg]), ("blocking", ["true"])] @
(if Option.map Bool.toString isar_proofs <> SOME isar_proofs_arg
@@ -516,7 +515,7 @@
|> map (normalize_raw_param ctxt)
val _ =
- run_sledgehammer (get_params mode ctxt override_params) mode (SOME output_result) 1
+ run_sledgehammer (get_params Normal ctxt override_params) Normal (SOME output_result) 1
no_fact_override (minimize_command override_params 1) state
in () end
| NONE => error "Unknown proof context"));
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Sat Aug 17 14:13:18 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Sat Aug 17 19:13:28 2013 +0200
@@ -13,7 +13,7 @@
val string_of_reconstructor : reconstructor -> string
- val one_line_proof_text : Properties.T -> int -> one_line_params -> string
+ val one_line_proof_text : int -> one_line_params -> string
val string_of_proof :
Proof.context -> string -> string -> int -> int -> isar_proof -> string
@@ -71,23 +71,24 @@
using_labels ls ^ apply_on_subgoal i n ^
command_call (string_of_reconstructor reconstr) ss
-fun try_command_line sendback_props banner time command =
+fun try_command_line banner time command =
banner ^ ": " ^
- Active.sendback_markup sendback_props command ^
+ Active.sendback_markup [Markup.padding_command] command ^
show_time time ^ "."
-fun minimize_line _ _ [] = ""
- | minimize_line sendback_props minimize_command ss =
+fun minimize_line _ [] = ""
+ | minimize_line minimize_command ss =
case minimize_command ss of
"" => ""
| command =>
- "\nTo minimize: " ^ Active.sendback_markup sendback_props command ^ "."
+ "\nTo minimize: " ^
+ Active.sendback_markup [Markup.padding_command] command ^ "."
fun split_used_facts facts =
facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
|> pairself (sort_distinct (string_ord o pairself fst))
-fun one_line_proof_text sendback_props num_chained
+fun one_line_proof_text num_chained
(preplay, banner, used_facts, minimize_command, subgoal,
subgoal_count) =
let
@@ -111,8 +112,8 @@
".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
\solve this.)"
else
- try_command_line sendback_props banner ext_time)
- in try_line ^ minimize_line sendback_props minimize_command (map fst (extra @ chained)) end
+ try_command_line banner ext_time)
+ in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Aug 17 14:13:18 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Aug 17 19:13:28 2013 +0200
@@ -16,7 +16,7 @@
type play = Sledgehammer_Reconstructor.play
type minimize_command = Sledgehammer_Reconstructor.minimize_command
- datatype mode = Auto_Try | Try | Normal | Normal_Result | MaSh | Auto_Minimize | Minimize
+ datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
type params =
{debug : bool,
@@ -161,7 +161,7 @@
(** The Sledgehammer **)
-datatype mode = Auto_Try | Try | Normal | Normal_Result | MaSh | Auto_Minimize | Minimize
+datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
(* Identifier that distinguishes Sledgehammer from other tools that could use
"Async_Manager". *)
@@ -464,11 +464,6 @@
| Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
| _ => "Try this"
-fun sendback_properties mode =
- if mode = Auto_Try orelse mode = Normal_Result
- then [Markup.padding_command]
- else []
-
fun bunch_of_reconstructors needs_full_types lam_trans =
if needs_full_types then
[Metis (full_type_enc, lam_trans false),
@@ -672,7 +667,6 @@
fun suffix_of_mode Auto_Try = "_try"
| suffix_of_mode Try = "_try"
| suffix_of_mode Normal = ""
- | suffix_of_mode Normal_Result = ""
| suffix_of_mode MaSh = ""
| suffix_of_mode Auto_Minimize = "_min"
| suffix_of_mode Minimize = "_min"
@@ -701,7 +695,6 @@
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
- val sendback_props = sendback_properties mode
val atp_mode =
if Config.get ctxt completish then Sledgehammer_Completish
else Sledgehammer
@@ -937,8 +930,8 @@
(output, run_time, used_from, atp_proof, outcome)) =
with_cleanup clean_up run () |> tap export
val important_message =
- if (mode = Normal orelse mode = Normal_Result) andalso
- random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
+ if mode = Normal andalso random_range 0 (atp_important_message_keep_quotient - 1) = 0
+ then
extract_important_message output
else
""
@@ -982,7 +975,7 @@
subgoal, subgoal_count)
val num_chained = length (#facts (Proof.goal state))
in
- proof_text ctxt sendback_props isar_proofs isar_params
+ proof_text ctxt isar_proofs isar_params
num_chained one_line_params
end,
(if verbose then
@@ -1160,7 +1153,6 @@
({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
val ctxt = Proof.context_of state
- val sendback_props = sendback_properties mode
fun weight_facts facts =
let val num_facts = length facts in
facts ~~ (0 upto num_facts - 1)
@@ -1188,7 +1180,7 @@
subgoal, subgoal_count)
val num_chained = length (#facts (Proof.goal state))
in
- one_line_proof_text sendback_props num_chained one_line_params
+ one_line_proof_text num_chained one_line_params
end,
if verbose then
"\nSMT solver real CPU time: " ^ string_of_time run_time ^ "."
@@ -1209,7 +1201,6 @@
({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...}
: prover_problem) =
let
- val sendback_props = sendback_properties mode
val reconstr =
if name = metisN then
Metis (type_enc |> the_default (hd partial_type_encs),
@@ -1236,7 +1227,7 @@
subgoal_count)
val num_chained = length (#facts (Proof.goal state))
in
- one_line_proof_text sendback_props num_chained one_line_params
+ one_line_proof_text num_chained one_line_params
end,
message_tail = ""}
| play =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sat Aug 17 14:13:18 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sat Aug 17 19:13:28 2013 +0200
@@ -25,9 +25,9 @@
Proof.context -> (string * stature) list vector -> 'a proof ->
string list option
val isar_proof_text :
- Proof.context -> Properties.T -> bool option -> isar_params -> one_line_params -> string
+ Proof.context -> bool option -> isar_params -> one_line_params -> string
val proof_text :
- Proof.context -> Properties.T -> bool option -> isar_params -> int -> one_line_params
+ Proof.context -> bool option -> isar_params -> int -> one_line_params
-> string
end;
@@ -412,7 +412,7 @@
* string Symtab.table * (string * stature) list vector
* (string * term) list * int Symtab.table * string proof * thm
-fun isar_proof_text ctxt sendback_props isar_proofs
+fun isar_proof_text ctxt isar_proofs
(debug, verbose, preplay_timeout, preplay_trace, isar_compress,
isar_compress_degree, merge_timeout_slack, isar_try0, isar_minimize, pool,
fact_names, lifted, sym_tab, atp_proof, goal)
@@ -425,7 +425,7 @@
|> (fn fixes =>
ctxt |> Variable.set_body false
|> Proof_Context.add_fixes fixes)
- val one_line_proof = one_line_proof_text sendback_props 0 one_line_params
+ val one_line_proof = one_line_proof_text 0 one_line_params
val type_enc =
if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
else partial_typesN
@@ -625,7 +625,7 @@
"\n\nStructured proof"
^ (commas msg |> not (null msg) ? enclose " (" ")")
^ ":\n" ^
- Active.sendback_markup sendback_props isar_text
+ Active.sendback_markup [Markup.padding_command] isar_text
end
end
val isar_proof =
@@ -645,12 +645,12 @@
| Trust_Playable _ => true
| Failed_to_Play _ => true
-fun proof_text ctxt sendback_props isar_proofs isar_params num_chained
+fun proof_text ctxt isar_proofs isar_params num_chained
(one_line_params as (preplay, _, _, _, _, _)) =
(if isar_proofs = SOME true orelse
(isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
- isar_proof_text ctxt sendback_props isar_proofs isar_params
+ isar_proof_text ctxt isar_proofs isar_params
else
- one_line_proof_text sendback_props num_chained) one_line_params
+ one_line_proof_text num_chained) one_line_params
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Aug 17 14:13:18 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Aug 17 19:13:28 2013 +0200
@@ -146,11 +146,11 @@
let
val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
val outcome =
- if outcome_code = someN orelse mode = Normal orelse mode = Normal_Result then
+ if outcome_code = someN orelse mode = Normal then
quote name ^ ": " ^ message ()
else ""
val _ =
- if outcome <> "" andalso mode = Normal_Result andalso is_some output_result then
+ if outcome <> "" andalso is_some output_result then
the output_result outcome
else
outcome
@@ -195,7 +195,8 @@
| n =>
let
val _ = Proof.assert_backward state
- val print = if mode = Normal then Output.urgent_message else K ()
+ val print =
+ if mode = Normal andalso is_none output_result then Output.urgent_message else K ()
val state =
state |> Proof.map_context (Config.put SMT_Config.verbose debug)
val ctxt = Proof.context_of state
@@ -284,7 +285,7 @@
|> Par_List.map (fn f => ignore (f (unknownN, state)))
handle ERROR msg => (print ("Error: " ^ msg); error msg)
fun maybe f (accum as (outcome_code, _)) =
- accum |> (mode = Normal orelse mode = Normal_Result orelse outcome_code <> someN) ? f
+ accum |> (mode = Normal orelse outcome_code <> someN) ? f
in
(unknownN, state)
|> (if blocking then
--- a/src/HOL/Tools/try0.ML Sat Aug 17 14:13:18 2013 +0200
+++ b/src/HOL/Tools/try0.ML Sat Aug 17 19:13:28 2013 +0200
@@ -137,7 +137,7 @@
Auto_Try => "Auto Try0 found a proof"
| Try => "Try0 found a proof"
| Normal => "Try this") ^ ": " ^
- Active.sendback_markup (if mode = Auto_Try then [Markup.padding_command] else [])
+ Active.sendback_markup [Markup.padding_command]
((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
"\n(" ^ space_implode "; " (map time_string xs) ^ ")."