# HG changeset patch
# User wenzelm
# Date 1274448560 -7200
# Node ID d01da9438170a2c56a88fe04031c39271f55c1e3
# Parent  1ce1b19f78f41f5736d702db2cc48ec4c7c5920b
added checkboxes for debug/tracing filter;
misc tuning;

diff -r 1ce1b19f78f4 -r d01da9438170 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri May 21 14:53:19 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri May 21 15:29:20 2010 +0200
@@ -28,15 +28,45 @@
   if (position == DockableWindowManager.FLOATING)
     setPreferredSize(new Dimension(500, 250))
 
-  val controls = new FlowPanel(FlowPanel.Alignment.Right)()
-  add(controls.peer, BorderLayout.NORTH)
-
   val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()))
   add(html_panel, BorderLayout.CENTER)
 
 
   /* controls */
 
+  private val zoom = Library.zoom_box(factor => { zoom_factor = factor; handle_resize() })
+  zoom.tooltip = "Zoom factor for basic font size"
+
+  private val update = new Button("Update") {
+    reactions += { case ButtonClicked(_) => handle_update() }
+  }
+  update.tooltip = "Update display according to state of command at caret position"
+
+  private val tracing = new CheckBox("Tracing") {
+    reactions += { case ButtonClicked(_) => handle_update() }
+  }
+  tracing.tooltip = "Indicate output of tracing messages"
+
+  private val debug = new CheckBox("Debug") {
+    reactions += { case ButtonClicked(_) => handle_update() }
+  }
+  debug.tooltip = "Indicate output of debug messages (usually disabled on the prover side)"
+
+  private val follow = new CheckBox("Follow")
+  follow.selected = true
+  follow.tooltip = "Indicate automatic update according to caret movement or state changes"
+
+  private def filtered_results(document: Document, cmd: Command): List[XML.Tree] =
+  {
+    val show_tracing = tracing.selected
+    val show_debug = debug.selected
+    document.current_state(cmd).results filter {
+      case Output.Message(Markup.TRACING, _, _) => show_tracing
+      case Output.Message(Markup.DEBUG, _, _) => show_debug
+      case _ => true
+    }
+  }
+
   private case class Render(body: List[XML.Tree])
 
   private def handle_update()
@@ -47,7 +77,7 @@
           val document = model.recent_document
           document.command_at(view.getTextArea.getCaretPosition) match {
             case Some((cmd, _)) =>
-              output_actor ! Render(document.current_state(cmd).results)
+              output_actor ! Render(filtered_results(document, cmd))
             case None =>
           }
         case None =>
@@ -62,18 +92,6 @@
       html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100))
     }
 
-  private val zoom = Library.zoom_box(factor => { zoom_factor = factor; handle_resize() })
-  zoom.tooltip = "Zoom factor for basic font size"
-
-  private val update = new Button("Update") {
-    reactions += { case ButtonClicked(_) => handle_update() }
-  }
-  update.tooltip = "Update display according to state of command at caret position"
-
-  private val follow = new CheckBox("Follow")
-  follow.tooltip = "Indicate automatic update according to caret movement or state changes"
-  follow.selected = true
-
 
   /* actor wiring */
 
@@ -88,7 +106,8 @@
             if (follow.selected) Document_Model(view.getBuffer) else None
           } match {
             case None =>
-            case Some(model) => html_panel.render(model.recent_document.current_state(cmd).results)
+            case Some(model) =>
+              html_panel.render(filtered_results(model.recent_document, cmd))
           }
 
         case bad => System.err.println("output_actor: ignoring bad message " + bad)
@@ -121,6 +140,8 @@
 
   /* init controls */
 
-  controls.contents ++= List(zoom, update, follow)
+  val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, update, debug, tracing, follow)
+  add(controls.peer, BorderLayout.NORTH)
+
   handle_update()
 }