refer to Simplifier Trace panel on first invocation;
authorwenzelm
Mon Jul 21 20:36:25 2014 +0200 (2014-07-21)
changeset 575963a1b1bda702f
parent 57595 e2305b9d1534
child 57597 5c3484b90d5c
refer to Simplifier Trace panel on first invocation;
src/Pure/Tools/simplifier_trace.ML
     1.1 --- a/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 17:39:20 2014 +0200
     1.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 20:36:25 2014 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  
     1.5  signature SIMPLIFIER_TRACE =
     1.6  sig
     1.7 -  val see_panel: unit -> unit
     1.8    val add_term_breakpoint: term -> Context.generic -> Context.generic
     1.9    val add_thm_breakpoint: thm -> Context.generic -> Context.generic
    1.10  end
    1.11 @@ -191,7 +190,7 @@
    1.12      val ((bg1, bg2), en) =
    1.13        YXML.output_markup_elem
    1.14          (Active.make_markup Markup.simp_trace_panelN {implicit = false, properties = []})
    1.15 -  in writeln ("See " ^ bg1 ^ bg2 ^ "simplifier trace" ^ en) end
    1.16 +  in "See " ^ bg1 ^ bg2 ^ "simplifier trace" ^ en end
    1.17  
    1.18  
    1.19  fun send_request (result_id, content) =
    1.20 @@ -299,7 +298,10 @@
    1.21    in
    1.22      (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of
    1.23        NONE => put 0
    1.24 -    | SOME res => (output_result res; put (#1 res)))
    1.25 +    | SOME res =>
    1.26 +       (if depth = 1 then writeln (see_panel ()) else ();
    1.27 +        output_result res;
    1.28 +        put (#1 res)))
    1.29    end
    1.30  
    1.31  fun indicate_failure ({term, ctxt, thm, rrule, ...}: data) ctxt' =