# HG changeset patch
# User wenzelm
# Date 1405957042 -7200
# Node ID 037f3b251df5b70796629d40fdd5794b1dc28dc4
# Parent  2f7d91242b999af7ad47de40cf4f7f631c26b106
regular message to refer to Simplifier Trace panel (unused);

diff -r 2f7d91242b99 -r 037f3b251df5 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Jul 21 16:58:12 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Mon Jul 21 17:37:22 2014 +0200
@@ -185,6 +185,7 @@
   val use_theories_result: string -> bool -> Properties.T
   val print_operationsN: string
   val print_operations: Properties.T
+  val simp_trace_panelN: string
   val simp_trace_logN: string
   val simp_trace_stepN: string
   val simp_trace_recurseN: string
@@ -586,6 +587,8 @@
 
 (* simplifier trace *)
 
+val simp_trace_panelN = "simp_trace_panel";
+
 val simp_trace_logN = "simp_trace_log";
 val simp_trace_stepN = "simp_trace_step";
 val simp_trace_recurseN = "simp_trace_recurse";
diff -r 2f7d91242b99 -r 037f3b251df5 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Mon Jul 21 16:58:12 2014 +0200
+++ b/src/Pure/PIDE/markup.scala	Mon Jul 21 17:37:22 2014 +0200
@@ -465,6 +465,7 @@
   /* simplifier trace */
 
   val SIMP_TRACE = "simp_trace"
+  val SIMP_TRACE_PANEL = "simp_trace_panel"
 
   val SIMP_TRACE_LOG = "simp_trace_log"
   val SIMP_TRACE_STEP = "simp_trace_step"
diff -r 2f7d91242b99 -r 037f3b251df5 src/Pure/Tools/simplifier_trace.ML
--- 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 () =
diff -r 2f7d91242b99 -r 037f3b251df5 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Mon Jul 21 16:58:12 2014 +0200
+++ b/src/Tools/jEdit/src/active.scala	Mon Jul 21 17:37:22 2014 +0200
@@ -48,6 +48,11 @@
                   Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
                 }
 
+              case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, _), _) =>
+                Swing_Thread.later {
+                  view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
+                }
+
               case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
                 props match {
                   case Position.Id(id) =>
diff -r 2f7d91242b99 -r 037f3b251df5 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Jul 21 16:58:12 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Jul 21 17:37:22 2014 +0200
@@ -149,7 +149,7 @@
 
   private val active_elements =
     Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
-      Markup.SENDBACK, Markup.SIMP_TRACE)
+      Markup.SENDBACK, Markup.SIMP_TRACE, Markup.SIMP_TRACE_PANEL)
 
   private val tooltip_message_elements =
     Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)