# HG changeset patch
# User blanchet
# Date 1306485008 -7200
# Node ID 1c451bbb3ad704f700fea69868c72be987b20315
# Parent  b10775a669d15708d549ae14e4b7e0e1a28a0919
repaired theory merging and defined/used helpers

diff -r b10775a669d1 -r 1c451bbb3ad7 src/Tools/try.ML
--- a/src/Tools/try.ML	Fri May 27 10:30:08 2011 +0200
+++ b/src/Tools/try.ML	Fri May 27 10:30:08 2011 +0200
@@ -13,6 +13,8 @@
   val tryN : string
   val auto_time_limit: real Unsynchronized.ref
 
+  val serial_commas : string -> string list -> string list
+  val subgoal_count : Proof.state -> int
   val register_tool : tool -> theory -> theory
   val get_tools : theory -> tool list
   val try_tools : Proof.state -> (string * string) option
@@ -39,31 +41,50 @@
       auto_try_time_limitN "Time limit for automatically tried tools (in seconds).")
 
 
+(* helpers *)
+
+fun serial_commas _ [] = ["??"]
+  | serial_commas _ [s] = [s]
+  | serial_commas conj [s1, s2] = [s1, conj, s2]
+  | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
+  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
+
+val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
+
+
 (* configuration *)
 
+val tool_ord = prod_ord int_ord string_ord o pairself (swap o apsnd #1)
+
 structure Data = Theory_Data
 (
   type T = tool list
   val empty = []
   val extend = I
-  fun merge data : T = AList.merge (op =) (K true) data
+  fun merge data : T = Ord_List.merge tool_ord data
 )
 
 val get_tools = Data.get
 
-val register_tool = Data.map o Ord_List.insert (int_ord o pairself (#1 o snd))
+val register_tool = Data.map o Ord_List.insert tool_ord
 
 (* try command *)
 
 fun try_tools state =
-  get_tools (Proof.theory_of state)
-  |> tap (fn tools => "Trying " ^ commas_quote (map fst tools) ^ "..."
-                      |> Output.urgent_message)
-  |> Par_List.get_some
-         (fn (name, (_, _, tool)) =>
-             case try (tool false) state of
-               SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
-             | _ => NONE)
+  if subgoal_count state = 0 then
+    (Output.urgent_message "No subgoal!"; NONE)
+  else
+    get_tools (Proof.theory_of state)
+    |> tap (fn tools =>
+               "Trying " ^ space_implode " "
+                    (serial_commas "and" (map (quote o fst) tools)) ^ "..."
+               |> Output.urgent_message)
+    |> Par_List.get_some
+           (fn (name, (_, _, tool)) =>
+               case try (tool false) state of
+                 SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
+               | _ => NONE)
+    |> tap (fn NONE => Output.urgent_message "Tried in vain." | _ => ())
 
 val _ =
   Outer_Syntax.improper_command tryN