1.1 --- a/src/HOL/Tools/try0.ML	Fri Nov 08 08:59:54 2013 +0100
     1.2 +++ b/src/HOL/Tools/try0.ML	Fri Nov 08 19:03:14 2013 +0100
     1.3 @@ -41,10 +41,10 @@
     1.4    end
     1.5    handle TimeLimit.TimeOut => false
     1.6  
     1.7 -fun do_generic timeout_opt command pre post apply st =
     1.8 +fun do_generic timeout_opt name command pre post apply st =
     1.9    let val timer = Timer.startRealTimer () in
    1.10      if can_apply timeout_opt pre post apply st then
    1.11 -      SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
    1.12 +      SOME (name, command, Time.toMilliseconds (Timer.checkRealTimer timer))
    1.13      else
    1.14        NONE
    1.15    end
    1.16 @@ -75,16 +75,11 @@
    1.17                      timeout_opt quad st =
    1.18    if mode <> Auto_Try orelse run_if_auto_try then
    1.19      let val attrs = attrs_text attrs quad in
    1.20 -      do_generic timeout_opt
    1.21 -                 (name ^ attrs ^
    1.22 -                  (if all_goals andalso
    1.23 -                      nprems_of (#goal (Proof.goal st)) > 1 then
    1.24 -                     " [1]"
    1.25 -                   else
    1.26 -                     ""))
    1.27 -                 I (#goal o Proof.goal)
    1.28 -                 (apply_named_method_on_first_goal (name ^ attrs)
    1.29 -                                                   (Proof.theory_of st)) st
    1.30 +      do_generic timeout_opt name
    1.31 +        ((name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
    1.32 +         (if all_goals andalso nprems_of (#goal (Proof.goal st)) > 1 then "[1]" else ""))
    1.33 +        I (#goal o Proof.goal)
    1.34 +        (apply_named_method_on_first_goal (name ^ attrs) (Proof.theory_of st)) st
    1.35      end
    1.36    else
    1.37      NONE
    1.38 @@ -116,7 +111,7 @@
    1.39      val st = st |> Proof.map_context (Config.put Metis_Tactic.verbose false #>
    1.40        Config.put Lin_Arith.verbose false)
    1.41      fun par_map f =
    1.42 -      if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o pairself snd)
    1.43 +      if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o pairself #3)
    1.44        else Par_List.get_some f #> the_list
    1.45    in
    1.46      if mode = Normal then
    1.47 @@ -125,16 +120,15 @@
    1.48        |> Output.urgent_message
    1.49      else
    1.50        ();
    1.51 -    case par_map (fn f => f mode timeout_opt quad st) do_methods of
    1.52 +    (case par_map (fn f => f mode timeout_opt quad st) do_methods of
    1.53        [] =>
    1.54        (if mode = Normal then Output.urgent_message "No proof found." else ();
    1.55         (false, (noneN, st)))
    1.56 -    | xs as (s, _) :: _ =>
    1.57 +    | xs as (name, command, _) :: _ =>
    1.58        let
    1.59 -        val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
    1.60 +        val xs = xs |> map (fn (name, _, n) => (n, name))
    1.61                      |> AList.coalesce (op =)
    1.62                      |> map (swap o apsnd commas)
    1.63 -        val need_parens = exists_string (curry (op =) " ") s
    1.64          val message =
    1.65            (case mode of
    1.66               Auto_Try => "Auto Try0 found a proof"
    1.67 @@ -142,18 +136,18 @@
    1.68             | Normal => "Try this") ^ ": " ^
    1.69            Active.sendback_markup [Markup.padding_command]
    1.70                ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
    1.71 -                else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
    1.72 +                else "apply") ^ " " ^ command) ^
    1.73            (case xs of
    1.74              [(_, ms)] => " (" ^ time_string ms ^ ")."
    1.75            | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ").")
    1.76        in
    1.77 -        (true, (s, st |> (if mode = Auto_Try then
    1.78 -                            Proof.goal_message
    1.79 -                                (fn () => Pretty.markup Markup.information
    1.80 -                                                        [Pretty.str message])
    1.81 -                          else
    1.82 -                            tap (fn _ => Output.urgent_message message))))
    1.83 -      end
    1.84 +        (true, (name,
    1.85 +           st |> (if mode = Auto_Try then
    1.86 +                    Proof.goal_message
    1.87 +                      (fn () => Pretty.markup Markup.information [Pretty.str message])
    1.88 +                  else
    1.89 +                    tap (fn _ => Output.urgent_message message))))
    1.90 +      end)
    1.91    end
    1.92  
    1.93  fun try0 timeout_opt = fst oo do_try0 Normal timeout_opt