1.1 --- a/src/Tools/try.ML	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/src/Tools/try.ML	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -13,6 +13,8 @@
     1.4    val tryN : string
     1.5    val auto_time_limit: real Unsynchronized.ref
     1.6  
     1.7 +  val serial_commas : string -> string list -> string list
     1.8 +  val subgoal_count : Proof.state -> int
     1.9    val register_tool : tool -> theory -> theory
    1.10    val get_tools : theory -> tool list
    1.11    val try_tools : Proof.state -> (string * string) option
    1.12 @@ -39,31 +41,50 @@
    1.13        auto_try_time_limitN "Time limit for automatically tried tools (in seconds).")
    1.14  
    1.15  
    1.16 +(* helpers *)
    1.17 +
    1.18 +fun serial_commas _ [] = ["??"]
    1.19 +  | serial_commas _ [s] = [s]
    1.20 +  | serial_commas conj [s1, s2] = [s1, conj, s2]
    1.21 +  | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
    1.22 +  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
    1.23 +
    1.24 +val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
    1.25 +
    1.26 +
    1.27  (* configuration *)
    1.28  
    1.29 +val tool_ord = prod_ord int_ord string_ord o pairself (swap o apsnd #1)
    1.30 +
    1.31  structure Data = Theory_Data
    1.32  (
    1.33    type T = tool list
    1.34    val empty = []
    1.35    val extend = I
    1.36 -  fun merge data : T = AList.merge (op =) (K true) data
    1.37 +  fun merge data : T = Ord_List.merge tool_ord data
    1.38  )
    1.39  
    1.40  val get_tools = Data.get
    1.41  
    1.42 -val register_tool = Data.map o Ord_List.insert (int_ord o pairself (#1 o snd))
    1.43 +val register_tool = Data.map o Ord_List.insert tool_ord
    1.44  
    1.45  (* try command *)
    1.46  
    1.47  fun try_tools state =
    1.48 -  get_tools (Proof.theory_of state)
    1.49 -  |> tap (fn tools => "Trying " ^ commas_quote (map fst tools) ^ "..."
    1.50 -                      |> Output.urgent_message)
    1.51 -  |> Par_List.get_some
    1.52 -         (fn (name, (_, _, tool)) =>
    1.53 -             case try (tool false) state of
    1.54 -               SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
    1.55 -             | _ => NONE)
    1.56 +  if subgoal_count state = 0 then
    1.57 +    (Output.urgent_message "No subgoal!"; NONE)
    1.58 +  else
    1.59 +    get_tools (Proof.theory_of state)
    1.60 +    |> tap (fn tools =>
    1.61 +               "Trying " ^ space_implode " "
    1.62 +                    (serial_commas "and" (map (quote o fst) tools)) ^ "..."
    1.63 +               |> Output.urgent_message)
    1.64 +    |> Par_List.get_some
    1.65 +           (fn (name, (_, _, tool)) =>
    1.66 +               case try (tool false) state of
    1.67 +                 SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
    1.68 +               | _ => NONE)
    1.69 +    |> tap (fn NONE => Output.urgent_message "Tried in vain." | _ => ())
    1.70  
    1.71  val _ =
    1.72    Outer_Syntax.improper_command tryN