# HG changeset patch
# User blanchet
# Date 1383584927 -3600
# Node ID c7af3d651658b87fdff1b22e520b4e9eecf1e4ba
# Parent  81ee85f56e2d67483d40948ac9b0471cd72b2b91
make 'try0' return faster when invoked as part of 'try'

diff -r 81ee85f56e2d -r c7af3d651658 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Mon Nov 04 17:25:36 2013 +0100
+++ b/src/HOL/Tools/try0.ML	Mon Nov 04 18:08:47 2013 +0100
@@ -108,12 +108,16 @@
    ("presburger", ((false, true), no_attrs))]
 val do_methods = map do_named_method named_methods
 
-fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
+fun time_string ms = string_of_int ms ^ " ms"
+fun tool_time_string (s, ms) = s ^ ": " ^ time_string ms
 
 fun do_try0 mode timeout_opt quad st =
   let
     val st = st |> Proof.map_context (Config.put Metis_Tactic.verbose false #>
       Config.put Lin_Arith.verbose false)
+    fun par_map f =
+      if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o pairself snd)
+      else Par_List.get_some f #> the_list
   in
     if mode = Normal then
       "Trying " ^ space_implode " " (Try.serial_commas "and"
@@ -121,8 +125,7 @@
       |> Output.urgent_message
     else
       ();
-    case do_methods |> Par_List.map (fn f => f mode timeout_opt quad st)
-                    |> map_filter I |> sort (int_ord o pairself snd) of
+    case par_map (fn f => f mode timeout_opt quad st) do_methods of
       [] =>
       (if mode = Normal then Output.urgent_message "No proof found." else ();
        (false, (noneN, st)))
@@ -140,7 +143,9 @@
           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) ^ ")."
+          (case xs of
+            [(_, ms)] => " (" ^ time_string ms ^ ")."
+          | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ").")
       in
         (true, (s, st |> (if mode = Auto_Try then
                             Proof.goal_message