# HG changeset patch
# User immler@in.tum.de
# Date 1233707928 -3600
# Node ID 7cd619ee3917b46ac05c91a5782b1a896125616e
# Parent  7407bc6cf28d00b2315c63e26da5a0b50b128f8e
removed redundant code

diff -r 7407bc6cf28d -r 7cd619ee3917 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Mon Feb 02 23:08:44 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Wed Feb 04 01:38:48 2009 +0100
@@ -85,30 +85,25 @@
     def to = Isabelle.prover_setup(buffer).get.theory_view.to_current(_)
     def from = Isabelle.prover_setup(buffer).get.theory_view.from_current(_)
 
-    val commands = document.commands.dropWhile(_.stop <= from(start))
-    if(commands.hasNext) {
-      var next_x = start
-      for {
-        command <- commands.takeWhile(_.start < from(stop))
-        markup <- command.root_node.flatten
-        if(to(markup.abs_stop) > start)
-        if(to(markup.abs_start) < stop)
-        byte = DynamicTokenMarker.choose_byte(markup.kind)
-        token_start = to(markup.abs_start) - start max 0
-        token_length = to(markup.abs_stop) - to(markup.abs_start) -
-                       (start - to(markup.abs_start) max 0) -
-                       (to(markup.abs_stop) - stop max 0)
-      } {
-        if (start + token_start > next_x) 
-          handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context)
-        handler.handleToken(line_segment, byte, token_start, token_length, context)
-        next_x = start + token_start + token_length
-      }
-      if (next_x < stop)
-        handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
-    } else {
-      handler.handleToken(line_segment, 1, 0, line_segment.count, context)
+    var next_x = start
+    for {
+      command <- document.commands.dropWhile(_.stop <= from(start)).takeWhile(_.start < from(stop))
+      markup <- command.root_node.flatten
+      if(to(markup.abs_stop) > start)
+      if(to(markup.abs_start) < stop)
+      byte = DynamicTokenMarker.choose_byte(markup.kind)
+      token_start = to(markup.abs_start) - start max 0
+      token_length = to(markup.abs_stop) - to(markup.abs_start) -
+                     (start - to(markup.abs_start) max 0) -
+                     (to(markup.abs_stop) - stop max 0)
+    } {
+      if (start + token_start > next_x)
+        handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context)
+      handler.handleToken(line_segment, byte, token_start, token_length, context)
+      next_x = start + token_start + token_length
     }
+    if (next_x < stop)
+      handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
 
     handler.handleToken(line_segment,Token.END, line_segment.count, 0, context)
     handler.setLineContext(context)