--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Tue Jun 02 19:40:20 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Tue Jun 02 22:22:03 2009 +0200
@@ -84,21 +84,25 @@
def from: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.from_current(document.id, _)
var next_x = start
- for {
- command <- document.commands.dropWhile(_.stop(document) <= from(start)).takeWhile(_.start(document) < from(stop))
- markup <- command.highlight_node.flatten
- if(to(markup.abs_stop(document)) > start)
- if(to(markup.abs_start(document)) < stop)
- byte = DynamicTokenMarker.choose_byte(markup.info.toString)
- token_start = to(markup.abs_start(document)) - start max 0
- token_length = to(markup.abs_stop(document)) - to(markup.abs_start(document)) -
- (start - to(markup.abs_start(document)) max 0) -
- (to(markup.abs_stop(document)) - 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
+
+ var command = document.find_command_at(from(start))
+ while (command != null && command.start(document) < from(stop)) {
+ for {
+ markup <- command.highlight_node.flatten
+ if(to(markup.abs_stop(document)) > start)
+ if(to(markup.abs_start(document)) < stop)
+ byte = DynamicTokenMarker.choose_byte(markup.info.toString)
+ token_start = to(markup.abs_start(document)) - start max 0
+ token_length = to(markup.abs_stop(document)) - to(markup.abs_start(document)) -
+ (start - to(markup.abs_start(document)) max 0) -
+ (to(markup.abs_stop(document)) - 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
+ }
+ command = document.commands.next(command).getOrElse(null)
}
if (next_x < stop)
handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Jun 02 19:40:20 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Jun 02 22:22:03 2009 +0200
@@ -193,14 +193,14 @@
val saved_color = gfx.getColor
val metrics = text_area.getPainter.getFontMetrics
+
+ // encolor phase
var e = document.find_command_at(from_current(start))
- val commands = document.commands.dropWhile(_.stop(document) <= from_current(start)).
- takeWhile(c => to_current(c.start(document)) < end)
- // encolor phase
- for (e <- commands) {
+ while (e != null && e.start(document) < end) {
val begin = start max to_current(e.start(document))
val finish = end - 1 min to_current(e.stop(document))
encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
+ e = document.commands.next(e).getOrElse(null)
}
gfx.setColor(saved_color)
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Tue Jun 02 19:40:20 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Tue Jun 02 22:22:03 2009 +0200
@@ -141,11 +141,6 @@
/** command view **/
- def find_command_at(pos: Int): Command = {
- for (cmd <- commands) { if (pos < cmd.stop(this)) return cmd }
- return null
- }
-
private def token_changed(new_id: String,
before_change: Option[Token],
inserted_tokens: List[Token],
@@ -223,4 +218,30 @@
new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset, active, is_command_keyword)
return (doc, change)
}
+
+ val commands_offsets = {
+ var last_stop = 0
+ (for (c <- commands) yield {
+ val r = c -> (last_stop,c.stop(this))
+ last_stop = c.stop(this)
+ r
+ }).toArray
+ }
+
+ // use a binary search to find commands for a given offset
+ def find_command_at(pos: Int): Command = find_command_at(pos, 0, commands_offsets.length)
+ private def find_command_at(pos: Int, array_start: Int, array_stop: Int): Command = {
+ val middle_index = (array_start + array_stop) / 2
+ if (middle_index >= commands_offsets.length) return null
+ val (middle, (start, stop)) = commands_offsets(middle_index)
+ // does middle contain pos?
+ if (start <= pos && stop > pos)
+ middle
+ else if (start > pos)
+ find_command_at(pos, array_start, middle_index)
+ else if (stop <= pos)
+ find_command_at(pos, middle_index + 1, array_stop)
+ else error("can't be")
+ }
+
}