--- a/src/Pure/Tools/simplifier_trace.ML Mon Jul 21 16:58:12 2014 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML Mon Jul 21 17:37:22 2014 +0200
@@ -6,6 +6,7 @@
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
@@ -185,6 +186,14 @@
(** tracing output **)
+fun see_panel () =
+ let
+ 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
+
+
fun send_request (result_id, content) =
let
fun break () =