# HG changeset patch
# User immler@in.tum.de
# Date 1227983469 -3600
# Node ID a02d46bca7e4eb0ad2fe2c0e1b9c4550f8160006
# Parent  7b5f44553aaf2abc61ca76fee0b57b160bf07c5b
encoloring only details in the current line!

diff -r 7b5f44553aaf -r a02d46bca7e4 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
     }