# HG changeset patch
# User wenzelm
# Date 1283090238 -7200
# Node ID e54c33dbe77ca6b41166e490f06e958633be0c47
# Parent  a9e37daf5bd0538f0cb5e3a0b77401eb9a82727d
Document_Model.token_marker: misc tuning and simplification;

diff -r a9e37daf5bd0 -r e54c33dbe77c src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 29 15:09:11 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 29 15:57:18 2010 +0200
@@ -265,7 +265,6 @@
 
         val start = buffer.getLineStartOffset(line)
         val stop = start + line_segment.count
-        val range = Text.Range(start, stop)
 
         /* FIXME
         for (text_area <- Isabelle.jedit_text_areas(buffer)
@@ -288,21 +287,16 @@
             Document_Model.Token_Markup.token_style(name)
         }
 
-        var next_x = start
-        for (info <- snapshot.select_markup(range)(token_markup)(Token.NULL)) {
-          val Text.Range(abs_start, abs_stop) = info.range
-          val token_start = (abs_start - start) max 0
-          val token_length =
-            (abs_stop - abs_start) -
-            ((start - abs_start) max 0) -
-            ((abs_stop - stop) max 0)
-          if (start + token_start > next_x)  // FIXME ??
-            handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
-          handle_token(info.info, token_start, token_length)
-          next_x = start + token_start + token_length
+        var last = start
+        for (token <- snapshot.select_markup(Text.Range(start, stop))(token_markup)(Token.NULL)) {
+          val Text.Range(token_start, token_stop) = token.range
+          if (last < token_start)
+            handle_token(Token.COMMENT1, last - start, token_start - last)
+          handle_token(token.info, token_start - start, token_stop - token_start)
+          last = token_stop
         }
-        if (next_x < stop)  // FIXME ??
-          handle_token(Token.COMMENT1, next_x - start, stop - next_x)
+        if (last < stop)
+          handle_token(Token.COMMENT1, last - start, stop - last)
 
         handle_token(Token.END, line_segment.count, 0)
         handler.setLineContext(context)