# HG changeset patch
# User immler@in.tum.de
# Date 1242992615 -7200
# Node ID d86023e76d3f786d27a9f884fcb7fc1a537bc324
# Parent  850dc36d49264f034ff7781fdd6db19c99e94bc3
removed debug-painting

diff -r 850dc36d4926 -r d86023e76d3f src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Fri May 22 13:43:35 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Fri May 22 13:43:35 2009 +0200
@@ -197,16 +197,6 @@
       val begin = start max to_current(e.start(document))
       val finish = end - 1 min to_current(e.stop(document))
       encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
-
-      // paint details of command
-      for (node <- e.highlight_node.flatten) {
-        val begin = to_current(node.abs_start(document))
-        val finish = to_current(node.abs_stop(document))
-        if (finish > start && begin < end) {
-          encolor(gfx, y + metrics.getHeight - 2, 1, begin max start, finish min end - 1,
-            DynamicTokenMarker.choose_color(node.info.toString, text_area.getPainter.getStyles), true)
-        }
-      }
     }
 
     gfx.setColor(saved_color)