encoloring only details in the current line!
authorimmler@in.tum.de
Sat, 29 Nov 2008 19:31:09 +0100
changeset 34392 a02d46bca7e4
parent 34391 7b5f44553aaf
child 34393 f0e1608a774f
encoloring only details in the current line!
src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Fri Nov 28 17:49:39 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Sat Nov 29 19:31:09 2008 +0100
@@ -187,16 +187,17 @@
 
     //Encolor Phase
     while (e != null && toCurrent(e.start) < end) {
-      val begin = Math.max(start, toCurrent(e.start))
-      val finish = Math.min(end - 1, toCurrent(e.stop))
+      val begin =  start max toCurrent(e.start)
+      val finish = end - 1 min  toCurrent(e.stop)
       encolor(gfx, y, fm.getHeight, begin, finish, chooseColor(e))
       // paint details of command
       var dy = 0
       for(status <- e.statuses){
         dy += 1
-        val begin = Math.max(start, toCurrent(status.start + e.start))
-        val finish = Math.min(end - 1, toCurrent(status.stop + e.start))
-        encolor(gfx, y + dy, fm.getHeight - dy, begin, finish, chooseColor(status.kind))
+        val begin = toCurrent(status.start + e.start)
+        val finish = toCurrent(status.stop + e.start)
+        if(finish > start && begin < end)
+          encolor(gfx, y + dy, fm.getHeight - dy, begin max start, finish min end, chooseColor(status.kind))
       }
       e = e.next
     }