# HG changeset patch # User immler@in.tum.de # Date 1243976113 -7200 # Node ID a0c84b0edb9a5410551d4299bdb88ec890398a43 # Parent 72b02f9c509c983b35ffae91caa75c33dd801cc4# Parent 2b46d92e46429341b3fdfa05283a0e4b63324427 merged; resolved superficial conflicts diff -r 72b02f9c509c -r a0c84b0edb9a src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala --- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Tue Jun 02 22:00:28 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Tue Jun 02 22:55:13 2009 +0200 @@ -84,24 +84,26 @@ 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) diff -r 72b02f9c509c -r a0c84b0edb9a src/Tools/jEdit/src/jedit/ProverSetup.scala --- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Tue Jun 02 22:00:28 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Tue Jun 02 22:55:13 2009 +0200 @@ -43,8 +43,11 @@ if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length) else path) theory_view.activate - prover ! new isabelle.proofdocument.Text.Change( - Isabelle.plugin.id(), 0, buffer.getText(0, buffer.getLength), 0) + val MCL = TheoryView.MAX_CHANGE_LENGTH + for (i <- 0 to buffer.getLength / MCL) + prover ! new isabelle.proofdocument.Text.Change( + Isabelle.plugin.id(), i * MCL, + buffer.getText(i * MCL, MCL min buffer.getLength - i * MCL),0) //register output-view prover.output_info += (text => diff -r 72b02f9c509c -r a0c84b0edb9a src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Jun 02 22:00:28 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Jun 02 22:55:13 2009 +0200 @@ -195,14 +195,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) diff -r 72b02f9c509c -r a0c84b0edb9a src/Tools/jEdit/src/proofdocument/ProofDocument.scala --- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Tue Jun 02 22:00:28 2009 +0200 +++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Tue Jun 02 22:55:13 2009 +0200 @@ -61,7 +61,7 @@ return (doc.mark_active, change) } def set_command_keyword(f: String => Boolean): ProofDocument = - new ProofDocument(id, tokens, token_start, commands, active, f) + new ProofDocument(isabelle.jedit.Isabelle.plugin.id(), tokens, token_start, commands, active, f) def content = Token.string_from_tokens(Nil ++ tokens, token_start) /** token view **/ @@ -126,7 +126,8 @@ case t :: ts => if (start(t) == start(new_token) && start(t) > change.start + change.added.length) { - old_suffix = ts + old_suffix = t :: ts + new_tokens = new_tokens.tail invalid_tokens = Nil } case _ => @@ -134,42 +135,45 @@ } val insert = new_tokens.reverse val new_token_list = begin ::: insert ::: old_suffix - val new_tokenset = (LinearSet() ++ new_token_list).asInstanceOf[LinearSet[Token]] token_changed(change.id, begin.lastOption, insert, - old_suffix.firstOption, new_tokenset, start) + old_suffix.firstOption, new_token_list, start) } /** 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], after_change: Option[Token], - new_tokenset: LinearSet[Token], + new_tokens: List[Token], new_token_start: Map[Token, Int]): (ProofDocument, StructureChange) = { - val cmd_first_changed = - if (before_change.isDefined) commands.find(_.tokens.contains(before_change.get)) - else None - val cmd_last_changed = - if (after_change.isDefined) commands.find(_.tokens.contains(after_change.get)) - else None + val new_tokenset = (LinearSet() ++ new_tokens).asInstanceOf[LinearSet[Token]] + val cmd_before_change = before_change match { + case None => None + case Some(bc) => + val cmd_with_bc = commands.find(_.contains(bc)).get + if (cmd_with_bc.tokens.last == bc) { + if (new_tokenset.next(bc).map(_.is_start).getOrElse(true)) + Some(cmd_with_bc) + else commands.prev(cmd_with_bc) + } + else commands.prev(cmd_with_bc) + } - val cmd_before_change = - if (cmd_first_changed.isDefined) commands.prev(cmd_first_changed.get) - else None - val cmd_after_change = - if (cmd_last_changed.isDefined) commands.next(cmd_last_changed.get) - else None + val cmd_after_change = after_change match { + case None => None + case Some(ac) => + val cmd_with_ac = commands.find(_.contains(ac)).get + if (ac.is_start) + Some(cmd_with_ac) + else + commands.next(cmd_with_ac) + } - val removed_commands = commands.dropWhile(Some(_) != cmd_first_changed). + val removed_commands = commands.dropWhile(Some(_) != cmd_before_change).drop(1). takeWhile(Some(_) != cmd_after_change) // calculate inserted commands @@ -183,21 +187,33 @@ } } - val split_begin_tokens = - if (!cmd_first_changed.isDefined || !before_change.isDefined) Nil - else { - cmd_first_changed.get.tokens.takeWhile(_ != before_change.get) ::: - List(before_change.get) - } - val split_end_tokens = - if (!cmd_last_changed.isDefined || !after_change.isDefined) Nil - else { - cmd_last_changed.get.tokens.dropWhile(_ != after_change.get) - } + val split_begin = + if (before_change.isDefined) { + val changed = + if (cmd_before_change.isDefined) + new_tokens.dropWhile(_ != cmd_before_change.get.tokens.last).drop(1) + else new_tokenset + if (changed.exists(_ == before_change.get)) + changed.takeWhile(_ != before_change.get).toList ::: + List(before_change.get) + else Nil + } else Nil + val split_end = + if (after_change.isDefined && cmd_after_change.isDefined) { + val unchanged = new_tokens.dropWhile(_ != after_change.get) + if (unchanged.exists(_ == cmd_after_change.get.tokens.first)) + unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList + else Nil + } else Nil + + val rescan_begin = + split_begin ::: + before_change.map(bc => new_tokens.dropWhile(_ != bc).drop(1)).getOrElse(new_tokens) val rescanning_tokens = - split_begin_tokens ::: inserted_tokens ::: split_end_tokens - val inserted_commands = tokens_to_commands(rescanning_tokens) + after_change.map(ac => rescan_begin.takeWhile(_ != ac)).getOrElse(rescan_begin) ::: + split_end + val inserted_commands = tokens_to_commands(rescanning_tokens.toList) val change = new StructureChange(cmd_before_change, inserted_commands, removed_commands.toList) // build new document @@ -209,4 +225,30 @@ 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") + } + } diff -r 72b02f9c509c -r a0c84b0edb9a src/Tools/jEdit/src/proofdocument/Token.scala --- a/src/Tools/jEdit/src/proofdocument/Token.scala Tue Jun 02 22:00:28 2009 +0200 +++ b/src/Tools/jEdit/src/proofdocument/Token.scala Tue Jun 02 22:55:13 2009 +0200 @@ -32,6 +32,8 @@ } class Token(val content: String, val kind: Token.Kind.Value) { + import Token.Kind._ val length = content.length override def toString = content + val is_start = kind == COMMAND_START || kind == COMMENT } diff -r 72b02f9c509c -r a0c84b0edb9a src/Tools/jEdit/src/prover/Command.scala --- a/src/Tools/jEdit/src/prover/Command.scala Tue Jun 02 22:00:28 2009 +0200 +++ b/src/Tools/jEdit/src/prover/Command.scala Tue Jun 02 22:55:13 2009 +0200 @@ -43,6 +43,8 @@ def start(doc: ProofDocument) = doc.token_start(tokens.first) def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length + def contains(p: Token) = tokens.contains(p) + /* command status */ var state_id: IsarDocument.State_ID = null diff -r 72b02f9c509c -r a0c84b0edb9a src/Tools/jEdit/src/prover/MarkupNode.scala --- a/src/Tools/jEdit/src/prover/MarkupNode.scala Tue Jun 02 22:00:28 2009 +0200 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Tue Jun 02 22:55:13 2009 +0200 @@ -125,8 +125,8 @@ } else this set_children new_children } else { - error("ignored nonfitting markup " + new_child.id + new_child.content + - new_child.info.toString + "(" +new_child.start + ", "+ new_child.stop + ")") + System.err.println("ignored nonfitting markup: " + new_child) + this } }