1.1 --- a/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 16:58:12 2014 +0200
     1.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 17:37:22 2014 +0200
     1.3 @@ -6,6 +6,7 @@
     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 @@ -185,6 +186,14 @@
    1.12  
    1.13  (** tracing output **)
    1.14  
    1.15 +fun see_panel () =
    1.16 +  let
    1.17 +    val ((bg1, bg2), en) =
    1.18 +      YXML.output_markup_elem
    1.19 +        (Active.make_markup Markup.simp_trace_panelN {implicit = false, properties = []})
    1.20 +  in writeln ("See " ^ bg1 ^ bg2 ^ "simplifier trace" ^ en) end
    1.21 +
    1.22 +
    1.23  fun send_request (result_id, content) =
    1.24    let
    1.25      fun break () =