src/HOL/Tools/try0.ML
changeset 67225 cb34f5f49a08
parent 67149 e61557884799
child 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Tools/try0.ML	Mon Dec 18 16:58:13 2017 +0100
     1.2 +++ b/src/HOL/Tools/try0.ML	Tue Dec 19 14:51:27 2017 +0100
     1.3 @@ -122,9 +122,15 @@
     1.4    let
     1.5      val st = Proof.map_contexts (silence_methods false) st;
     1.6      fun trd (_, _, t) = t;
     1.7 -    fun par_map f =
     1.8 -      if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o apply2 trd)
     1.9 -      else Par_List.get_some f #> the_list;
    1.10 +    fun try_method method = method mode timeout_opt quad st;
    1.11 +    fun get_message (_, command, ms) = "Found proof: " ^ Active.sendback_markup_command
    1.12 +      ((if Thm.nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^ " " ^ command) ^
    1.13 +      " (" ^ time_string ms ^ ")";
    1.14 +    val print_step = Option.map (tap (writeln o get_message));
    1.15 +    val get_results =
    1.16 +      if mode = Normal
    1.17 +      then Par_List.map (try_method #> print_step) #> map_filter I #> sort (int_ord o apply2 trd)
    1.18 +      else Par_List.get_some try_method #> the_list;
    1.19    in
    1.20      if mode = Normal then
    1.21        "Trying " ^ space_implode " " (Try.serial_commas "and" (map (quote o fst) named_methods)) ^
    1.22 @@ -132,7 +138,7 @@
    1.23        |> writeln
    1.24      else
    1.25        ();
    1.26 -    (case par_map (fn f => f mode timeout_opt quad st) apply_methods of
    1.27 +    (case get_results apply_methods of
    1.28        [] =>
    1.29        (if mode = Normal then writeln "No proof found" else (); (false, (noneN, [])))
    1.30      | xs as (name, command, _) :: _ =>