src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
changeset 52697 6fb98a20c349
parent 52629 d6f2a7c196f7
child 52994 fcd3a59c6f72
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Jul 18 13:12:54 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Jul 18 20:53:22 2013 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5    val string_of_reconstructor : reconstructor -> string
     1.6  
     1.7 -  val one_line_proof_text : int -> one_line_params -> string
     1.8 +  val one_line_proof_text : bool -> int -> one_line_params -> string
     1.9  
    1.10    val string_of_proof :
    1.11      Proof.context -> string -> string -> int -> int -> isar_proof -> string
    1.12 @@ -71,21 +71,24 @@
    1.13    using_labels ls ^ apply_on_subgoal i n ^
    1.14    command_call (string_of_reconstructor reconstr) ss
    1.15  
    1.16 -fun try_command_line banner time command =
    1.17 -  banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "."
    1.18 +fun try_command_line auto banner time command =
    1.19 +  banner ^ ": " ^
    1.20 +  Active.sendback_markup (if auto then [Markup.padding_command] else []) command ^
    1.21 +  show_time time ^ "."
    1.22  
    1.23 -fun minimize_line _ [] = ""
    1.24 -  | minimize_line minimize_command ss =
    1.25 +fun minimize_line _ _ [] = ""
    1.26 +  | minimize_line auto minimize_command ss =
    1.27      case minimize_command ss of
    1.28        "" => ""
    1.29      | command =>
    1.30 -      "\nTo minimize: " ^ Active.sendback_markup command ^ "."
    1.31 +      "\nTo minimize: " ^
    1.32 +      Active.sendback_markup (if auto then [Markup.padding_command] else []) command ^ "."
    1.33  
    1.34  fun split_used_facts facts =
    1.35    facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
    1.36          |> pairself (sort_distinct (string_ord o pairself fst))
    1.37  
    1.38 -fun one_line_proof_text num_chained
    1.39 +fun one_line_proof_text auto num_chained
    1.40          (preplay, banner, used_facts, minimize_command, subgoal,
    1.41           subgoal_count) =
    1.42    let
    1.43 @@ -109,8 +112,8 @@
    1.44                       ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
    1.45                       \solve this.)"
    1.46            else
    1.47 -            try_command_line banner ext_time)
    1.48 -  in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
    1.49 +            try_command_line auto banner ext_time)
    1.50 +  in try_line ^ minimize_line auto minimize_command (map fst (extra @ chained)) end
    1.51  
    1.52  
    1.53