# HG changeset patch
# User wenzelm
# Date 1348839903 -7200
# Node ID 77a0a53caa2f87ab616cbe74a774c933957a5b41
# Parent  5a0817ec03145129a003c078a21f8ed916432d17
display number of tracing messages;

diff -r 5a0817ec0314 -r 77a0a53caa2f src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Fri Sep 28 15:25:49 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Sep 28 15:45:03 2012 +0200
@@ -34,6 +34,7 @@
   private var current_snapshot = Document.State.init.snapshot()
   private var current_state = Command.empty.init_state
   private var current_output: List[XML.Tree] = Nil
+  private var current_tracing = 0
 
 
   /* pretty text panel */
@@ -70,18 +71,28 @@
         case None => (current_snapshot, current_state)
       }
 
-    val new_output =
+    val (new_output, new_tracing) =
       if (!restriction.isDefined || restriction.get.contains(new_state.command))
-        new_state.results.iterator.map(_._2)
-          .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList  // FIXME not scalable
-      else current_output
+      {
+        val new_output =
+          new_state.results.iterator.map(_._2)
+            .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList  // FIXME not scalable
+        val new_tracing =
+          new_state.results.iterator.map(_._2).filter(Protocol.is_tracing(_)).length
+        (new_output, new_tracing)
+      }
+      else (current_output, current_tracing)
 
     if (new_output != current_output)
       pretty_text_area.update(new_snapshot, Library.separate(Pretty.Separator, new_output))
 
+    if (new_tracing != current_tracing)
+      tracing.text = tracing_text(new_tracing)
+
     current_snapshot = new_snapshot
     current_state = new_state
     current_output = new_output
+    current_tracing = new_tracing
   }
 
 
@@ -138,7 +149,10 @@
   private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
   zoom.tooltip = "Zoom factor for basic font size"
 
-  private val tracing = new CheckBox("Tracing") {
+  private def tracing_text(n: Int): String =
+    if (n == 0) "Tracing" else "Tracing (" + n.toString + ")"
+
+  private val tracing = new CheckBox(tracing_text(current_tracing)) {
     reactions += {
       case ButtonClicked(_) => show_tracing = this.selected; handle_update(do_update, None) }
   }