# HG changeset patch # User wenzelm # Date 1376759608 -7200 # Node ID a0db255af8c52b95b60b47c9c0f061b247cdc8f1 # Parent 1474d251b56241aeb2f3b9e35733bf2cbdc38b47 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; diff -r 1474d251b562 -r a0db255af8c5 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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")); diff -r 1474d251b562 -r a0db255af8c5 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML --- 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 diff -r 1474d251b562 -r a0db255af8c5 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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 => diff -r 1474d251b562 -r a0db255af8c5 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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; diff -r 1474d251b562 -r a0db255af8c5 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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 diff -r 1474d251b562 -r a0db255af8c5 src/HOL/Tools/try0.ML --- 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) ^ ")."