# HG changeset patch
# User wenzelm
# Date 1248429334 -7200
# Node ID 116461b8fc01d911e4b6fa5ab311609430e31b6b
# Parent  d32817dda0e64fb9e6706109b7776dbd85a1103c
eliminated print_goals_without_context -- proper pretty printing;

diff -r d32817dda0e6 -r 116461b8fc01 src/Pure/display_goal.ML
--- a/src/Pure/display_goal.ML	Fri Jul 24 11:50:35 2009 +0200
+++ b/src/Pure/display_goal.ML	Fri Jul 24 11:55:34 2009 +0200
@@ -13,7 +13,6 @@
   val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} ->
     thm -> Pretty.T list
   val pretty_goals_without_context: int -> thm -> Pretty.T list
-  val print_goals_without_context: int -> thm -> unit
 end;
 
 structure Display_Goal: DISPLAY_GOAL =
@@ -119,9 +118,6 @@
   pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th))
     {total = true, main = true, maxgoals = n} th;
 
-val print_goals_without_context =
-  (Pretty.writeln o Pretty.chunks) oo pretty_goals_without_context;
-
 end;
 
 end;
diff -r d32817dda0e6 -r 116461b8fc01 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Fri Jul 24 11:50:35 2009 +0200
+++ b/src/Pure/tctical.ML	Fri Jul 24 11:55:34 2009 +0200
@@ -232,9 +232,10 @@
 (*Extract from a tactic, a thm->thm seq function that handles tracing*)
 fun tracify flag tac st =
   if !flag andalso not (!suppress_tracing) then
-   (Display_Goal.print_goals_without_context (! Display_Goal.goals_limit) st;
-    tracing "** Press RETURN to continue:";
-    exec_trace_command flag (tac, st))
+    (tracing (Pretty.string_of (Pretty.chunks
+        (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st @
+          [Pretty.str "** Press RETURN to continue:"])));
+     exec_trace_command flag (tac, st))
   else tac st;
 
 (*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)