# HG changeset patch
# User wenzelm
# Date 1486235547 -3600
# Node ID 69592ac048368e97d62d8e3f2f9a99eb1f24af77
# Parent  2f72056cf78a648106fbfb82c8356aaf72fa9483
clarified message: print subgoal number instead of potentially large term;

diff -r 2f72056cf78a -r 69592ac04836 src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Sat Feb 04 19:53:41 2017 +0100
+++ b/src/Tools/solve_direct.ML	Sat Feb 04 20:12:27 2017 +0100
@@ -47,18 +47,12 @@
       #2 (Find_Theorems.find_theorems ctxt (SOME goal)
         (SOME (Config.get ctxt max_solutions)) false [(true, Find_Theorems.Solves)]);
 
-    fun prt_result (goal, results) =
-      let
-        val msg =
-          (if mode = Auto_Try then "Auto " else "") ^ solve_directN ^ ": " ^
-          (case goal of
-            NONE => "The current goal"
-          | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
-      in
-        Pretty.big_list
-          (msg ^ " can be solved directly with")
-          (map (Find_Theorems.pretty_thm ctxt) results)
-      end;
+    fun prt_result (subgoal, results) =
+      Pretty.big_list
+        ((if mode = Auto_Try then "Auto " else "") ^ solve_directN ^ ": " ^
+          (case subgoal of NONE => "the current goal" | SOME i => "subgoal #" ^ string_of_int i) ^
+          " can be solved directly with")
+        (map (Find_Theorems.pretty_thm ctxt) results);
 
     fun seek_against_goal () =
       (case try (#goal o Proof.simple_goal) state of
@@ -69,16 +63,16 @@
             val rs =
               if length subgoals = 1
               then [(NONE, find goal)]
-              else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
+              else map_index (fn (i, sg) => (SOME (i + 1), find (Goal.init sg))) subgoals;
             val results = filter_out (null o #2) rs;
           in if null results then NONE else SOME results end);
-    fun message results = separate (Pretty.brk 0) (map prt_result results);
   in
     (case try seek_against_goal () of
       SOME (SOME results) =>
         (someN,
           let
-            val msg = Pretty.string_of (Pretty.chunks (message results))
+            val chunks = separate (Pretty.str "") (map prt_result results);
+            val msg = Pretty.string_of (Pretty.chunks chunks);
           in
             if Config.get ctxt strict_warnings then (warning msg; [])
             else if mode = Auto_Try then [msg]