1.1 --- a/src/Pure/PIDE/markup.ML	Mon Jul 21 16:58:12 2014 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Mon Jul 21 17:37:22 2014 +0200
     1.3 @@ -185,6 +185,7 @@
     1.4    val use_theories_result: string -> bool -> Properties.T
     1.5    val print_operationsN: string
     1.6    val print_operations: Properties.T
     1.7 +  val simp_trace_panelN: string
     1.8    val simp_trace_logN: string
     1.9    val simp_trace_stepN: string
    1.10    val simp_trace_recurseN: string
    1.11 @@ -586,6 +587,8 @@
    1.12  
    1.13  (* simplifier trace *)
    1.14  
    1.15 +val simp_trace_panelN = "simp_trace_panel";
    1.16 +
    1.17  val simp_trace_logN = "simp_trace_log";
    1.18  val simp_trace_stepN = "simp_trace_step";
    1.19  val simp_trace_recurseN = "simp_trace_recurse";

     2.1 --- a/src/Pure/PIDE/markup.scala	Mon Jul 21 16:58:12 2014 +0200
     2.2 +++ b/src/Pure/PIDE/markup.scala	Mon Jul 21 17:37:22 2014 +0200
     2.3 @@ -465,6 +465,7 @@
     2.4    /* simplifier trace */
     2.5  
     2.6    val SIMP_TRACE = "simp_trace"
     2.7 +  val SIMP_TRACE_PANEL = "simp_trace_panel"
     2.8  
     2.9    val SIMP_TRACE_LOG = "simp_trace_log"
    2.10    val SIMP_TRACE_STEP = "simp_trace_step"

     3.1 --- a/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 16:58:12 2014 +0200
     3.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 17:37:22 2014 +0200
     3.3 @@ -6,6 +6,7 @@
     3.4  
     3.5  signature SIMPLIFIER_TRACE =
     3.6  sig
     3.7 +  val see_panel: unit -> unit
     3.8    val add_term_breakpoint: term -> Context.generic -> Context.generic
     3.9    val add_thm_breakpoint: thm -> Context.generic -> Context.generic
    3.10  end
    3.11 @@ -185,6 +186,14 @@
    3.12  
    3.13  (** tracing output **)
    3.14  
    3.15 +fun see_panel () =
    3.16 +  let
    3.17 +    val ((bg1, bg2), en) =
    3.18 +      YXML.output_markup_elem
    3.19 +        (Active.make_markup Markup.simp_trace_panelN {implicit = false, properties = []})
    3.20 +  in writeln ("See " ^ bg1 ^ bg2 ^ "simplifier trace" ^ en) end
    3.21 +
    3.22 +
    3.23  fun send_request (result_id, content) =
    3.24    let
    3.25      fun break () =

     4.1 --- a/src/Tools/jEdit/src/active.scala	Mon Jul 21 16:58:12 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/active.scala	Mon Jul 21 17:37:22 2014 +0200
     4.3 @@ -48,6 +48,11 @@
     4.4                    Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
     4.5                  }
     4.6  
     4.7 +              case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, _), _) =>
     4.8 +                Swing_Thread.later {
     4.9 +                  view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
    4.10 +                }
    4.11 +
    4.12                case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
    4.13                  props match {
    4.14                    case Position.Id(id) =>

     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Jul 21 16:58:12 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Jul 21 17:37:22 2014 +0200
     5.3 @@ -149,7 +149,7 @@
     5.4  
     5.5    private val active_elements =
     5.6      Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
     5.7 -      Markup.SENDBACK, Markup.SIMP_TRACE)
     5.8 +      Markup.SENDBACK, Markup.SIMP_TRACE, Markup.SIMP_TRACE_PANEL)
     5.9  
    5.10    private val tooltip_message_elements =
    5.11      Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)