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)