src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
changeset 34522 7cd619ee3917
parent 34518 7407bc6cf28d
child 34523 e19f33968557
equal deleted inserted replaced
34518:7407bc6cf28d 34522:7cd619ee3917
    83     val stop = start + line_segment.count
    83     val stop = start + line_segment.count
    84     
    84     
    85     def to = Isabelle.prover_setup(buffer).get.theory_view.to_current(_)
    85     def to = Isabelle.prover_setup(buffer).get.theory_view.to_current(_)
    86     def from = Isabelle.prover_setup(buffer).get.theory_view.from_current(_)
    86     def from = Isabelle.prover_setup(buffer).get.theory_view.from_current(_)
    87 
    87 
    88     val commands = document.commands.dropWhile(_.stop <= from(start))
    88     var next_x = start
    89     if(commands.hasNext) {
    89     for {
    90       var next_x = start
    90       command <- document.commands.dropWhile(_.stop <= from(start)).takeWhile(_.start < from(stop))
    91       for {
    91       markup <- command.root_node.flatten
    92         command <- commands.takeWhile(_.start < from(stop))
    92       if(to(markup.abs_stop) > start)
    93         markup <- command.root_node.flatten
    93       if(to(markup.abs_start) < stop)
    94         if(to(markup.abs_stop) > start)
    94       byte = DynamicTokenMarker.choose_byte(markup.kind)
    95         if(to(markup.abs_start) < stop)
    95       token_start = to(markup.abs_start) - start max 0
    96         byte = DynamicTokenMarker.choose_byte(markup.kind)
    96       token_length = to(markup.abs_stop) - to(markup.abs_start) -
    97         token_start = to(markup.abs_start) - start max 0
    97                      (start - to(markup.abs_start) max 0) -
    98         token_length = to(markup.abs_stop) - to(markup.abs_start) -
    98                      (to(markup.abs_stop) - stop max 0)
    99                        (start - to(markup.abs_start) max 0) -
    99     } {
   100                        (to(markup.abs_stop) - stop max 0)
   100       if (start + token_start > next_x)
   101       } {
   101         handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context)
   102         if (start + token_start > next_x) 
   102       handler.handleToken(line_segment, byte, token_start, token_length, context)
   103           handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context)
   103       next_x = start + token_start + token_length
   104         handler.handleToken(line_segment, byte, token_start, token_length, context)
       
   105         next_x = start + token_start + token_length
       
   106       }
       
   107       if (next_x < stop)
       
   108         handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
       
   109     } else {
       
   110       handler.handleToken(line_segment, 1, 0, line_segment.count, context)
       
   111     }
   104     }
       
   105     if (next_x < stop)
       
   106       handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
   112 
   107 
   113     handler.handleToken(line_segment,Token.END, line_segment.count, 0, context)
   108     handler.handleToken(line_segment,Token.END, line_segment.count, 0, context)
   114     handler.setLineContext(context)
   109     handler.setLineContext(context)
   115     return context
   110     return context
   116   }
   111   }