--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Fri Aug 16 23:11:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Sat Aug 17 11:34:50 2013 +0200
@@ -13,7 +13,7 @@
val string_of_reconstructor : reconstructor -> string
- val one_line_proof_text : bool -> int -> one_line_params -> string
+ val one_line_proof_text : Properties.T -> int -> one_line_params -> string
val string_of_proof :
Proof.context -> string -> string -> int -> int -> isar_proof -> string
@@ -71,25 +71,23 @@
using_labels ls ^ apply_on_subgoal i n ^
command_call (string_of_reconstructor reconstr) ss
-fun try_command_line auto banner time command =
+fun try_command_line sendback_props banner time command =
banner ^ ": " ^
- Active.sendback_markup (if auto then [Markup.padding_command] else []) command ^
+ Active.sendback_markup sendback_props command ^
show_time time ^ "."
fun minimize_line _ _ [] = ""
- | minimize_line auto minimize_command ss =
+ | minimize_line sendback_props minimize_command ss =
case minimize_command ss of
"" => ""
| command =>
- "\nTo minimize: " ^
- Active.sendback_markup (if auto then [Markup.padding_command] else [])
- command ^ "."
+ "\nTo minimize: " ^ Active.sendback_markup sendback_props 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 auto num_chained
+fun one_line_proof_text sendback_props num_chained
(preplay, banner, used_facts, minimize_command, subgoal,
subgoal_count) =
let
@@ -113,8 +111,8 @@
".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
\solve this.)"
else
- try_command_line auto banner ext_time)
- in try_line ^ minimize_line auto minimize_command (map fst (extra @ chained)) end
+ try_command_line sendback_props banner ext_time)
+ in try_line ^ minimize_line sendback_props minimize_command (map fst (extra @ chained)) end