# HG changeset patch
# User wenzelm
# Date 1405967785 -7200
# Node ID 3a1b1bda702f8a0bf5b14228f52f72b18f2bd910
# Parent  e2305b9d1534486022bf5e175ad8700eb2f57ae7
refer to Simplifier Trace panel on first invocation;

diff -r e2305b9d1534 -r 3a1b1bda702f src/Pure/Tools/simplifier_trace.ML
--- a/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 17:39:20 2014 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 20:36:25 2014 +0200
@@ -6,7 +6,6 @@
 
 signature SIMPLIFIER_TRACE =
 sig
-  val see_panel: unit -> unit
   val add_term_breakpoint: term -> Context.generic -> Context.generic
   val add_thm_breakpoint: thm -> Context.generic -> Context.generic
 end
@@ -191,7 +190,7 @@
     val ((bg1, bg2), en) =
       YXML.output_markup_elem
         (Active.make_markup Markup.simp_trace_panelN {implicit = false, properties = []})
-  in writeln ("See " ^ bg1 ^ bg2 ^ "simplifier trace" ^ en) end
+  in "See " ^ bg1 ^ bg2 ^ "simplifier trace" ^ en end
 
 
 fun send_request (result_id, content) =
@@ -299,7 +298,10 @@
   in
     (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of
       NONE => put 0
-    | SOME res => (output_result res; put (#1 res)))
+    | SOME res =>
+       (if depth = 1 then writeln (see_panel ()) else ();
+        output_result res;
+        put (#1 res)))
   end
 
 fun indicate_failure ({term, ctxt, thm, rrule, ...}: data) ctxt' =