removed debug-painting
authorimmler@in.tum.de
Fri, 22 May 2009 13:43:35 +0200
changeset 34568d86023e76d3f
parent 34567 850dc36d4926
child 34569 28fa2f219f01
removed debug-painting
src/Tools/jEdit/src/jedit/TheoryView.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Fri May 22 13:43:35 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Fri May 22 13:43:35 2009 +0200
     1.3 @@ -197,16 +197,6 @@
     1.4        val begin = start max to_current(e.start(document))
     1.5        val finish = end - 1 min to_current(e.stop(document))
     1.6        encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
     1.7 -
     1.8 -      // paint details of command
     1.9 -      for (node <- e.highlight_node.flatten) {
    1.10 -        val begin = to_current(node.abs_start(document))
    1.11 -        val finish = to_current(node.abs_stop(document))
    1.12 -        if (finish > start && begin < end) {
    1.13 -          encolor(gfx, y + metrics.getHeight - 2, 1, begin max start, finish min end - 1,
    1.14 -            DynamicTokenMarker.choose_color(node.info.toString, text_area.getPainter.getStyles), true)
    1.15 -        }
    1.16 -      }
    1.17      }
    1.18  
    1.19      gfx.setColor(saved_color)