# HG changeset patch # User immler@in.tum.de # Date 1240414549 -7200 # Node ID 7dc6c231da4065fc08f4c5197ef7e164f8d8da56 # Parent d013be0adb66087c2fa2798559838f5e266e9300 abs. stops, markup nodes depend on doc-version; fixed missing positions in ProofDocument.text_changed; relink only changed commands in ProofDocument.token_changed diff -r d013be0adb66 -r 7dc6c231da40 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala --- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Mon Apr 20 20:28:45 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Wed Apr 22 17:35:49 2009 +0200 @@ -74,22 +74,22 @@ val start = buffer.getLineStartOffset(line) val stop = start + line_segment.count - val current_document = prover.document - - def to: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.to_current(current_document.id, _) - def from: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.from_current(current_document.id, _) + val document = prover.document + + def to: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.to_current(document.id, _) + def from: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.from_current(document.id, _) var next_x = start for { - command <- current_document.commands.dropWhile(_.stop <= from(start)).takeWhile(_.start < from(stop)) + command <- document.commands.dropWhile(_.stop(document) <= from(start)).takeWhile(_.start(document) < from(stop)) markup <- command.root_node.flatten - if(to(markup.abs_stop) > start) - if(to(markup.abs_start) < stop) + if(to(markup.abs_stop(document)) > start) + if(to(markup.abs_start(document)) < 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) + 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) diff -r d013be0adb66 -r 7dc6c231da40 src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala --- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Mon Apr 20 20:28:45 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Wed Apr 22 17:35:49 2009 +0200 @@ -33,7 +33,7 @@ if (prover_setup.isDefined) { val document = prover_setup.get.prover.document for (command <- document.commands) - data.root.add(command.root_node.swing_node) + data.root.add(command.root_node.swing_node(document)) if (stopped) data.root.add(new DefaultMutableTreeNode("")) } else { diff -r d013be0adb66 -r 7dc6c231da40 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala --- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Mon Apr 20 20:28:45 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Wed Apr 22 17:35:49 2009 +0200 @@ -7,6 +7,7 @@ package isabelle.jedit import isabelle.prover.Command +import isabelle.proofdocument.ProofDocument import isabelle.utils.Delay import javax.swing._ @@ -57,9 +58,9 @@ } else "" } - private def paintCommand(command : Command, buffer : JEditBuffer, doc_id: String, gfx : Graphics) { - val line1 = buffer.getLineOfOffset(to_current(doc_id, command.start)) - val line2 = buffer.getLineOfOffset(to_current(doc_id, command.stop - 1)) + 1 + private def paintCommand(command : Command, buffer : JEditBuffer, doc: ProofDocument, gfx : Graphics) { + val line1 = buffer.getLineOfOffset(to_current(doc.id, command.start(doc))) + val line2 = buffer.getLineOfOffset(to_current(doc.id, command.stop(doc) - 1)) + 1 val y = lineToY(line1) val height = lineToY(line2) - y - 1 val (light, dark) = command.status match { @@ -82,7 +83,7 @@ val buffer = textarea.getBuffer val document = prover.document for (c <- document.commands) - paintCommand(c, buffer, document.id, gfx) + paintCommand(c, buffer, document, gfx) } diff -r d013be0adb66 -r 7dc6c231da40 src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Apr 20 20:28:45 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Wed Apr 22 17:35:49 2009 +0200 @@ -66,8 +66,9 @@ private val selected_state_controller = new CaretListener { override def caretUpdate(e: CaretEvent) = { - val cmd = prover.document.find_command_at(e.getDot) - if (cmd != null && cmd.start <= e.getDot && + val doc = prover.document + val cmd = doc.find_command_at(e.getDot) + if (cmd != null && doc.token_start(cmd.tokens.first) <= e.getDot && Isabelle.prover_setup(buffer).get.selected_state != cmd) Isabelle.prover_setup(buffer).get.selected_state = cmd } @@ -141,8 +142,8 @@ { val document = prover.document if (text_area != null) { - val start = text_area.getLineOfOffset(to_current(document.id, cmd.start)) - val stop = text_area.getLineOfOffset(to_current(document.id, cmd.stop) - 1) + val start = text_area.getLineOfOffset(to_current(document.id, cmd.start(document))) + val stop = text_area.getLineOfOffset(to_current(document.id, cmd.stop(document)) - 1) text_area.invalidateLineRange(start, stop) if (Isabelle.prover_setup(buffer).get.selected_state == cmd) @@ -189,18 +190,18 @@ val metrics = text_area.getPainter.getFontMetrics var e = document.find_command_at(from_current(start)) - val commands = document.commands.dropWhile(_.stop <= from_current(start)). - takeWhile(c => to_current(c.start) < end) + val commands = document.commands.dropWhile(_.stop(document) <= from_current(start)). + takeWhile(c => to_current(c.start(document)) < end) // encolor phase for (e <- commands) { - val begin = start max to_current(e.start) - val finish = end - 1 min to_current(e.stop) + 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) // paint details of command for (node <- e.root_node.dfs) { - val begin = to_current(node.start + e.start) - val finish = to_current(node.stop + e.start) + val begin = to_current(node.abs_start(document)) + val finish = to_current(node.abs_stop(document)) if (finish > start && begin < end) { encolor(gfx, y + metrics.getHeight - 2, 1, begin max start, finish min end - 1, DynamicTokenMarker.choose_color(node.kind, text_area.getPainter.getStyles), true) diff -r d013be0adb66 -r 7dc6c231da40 src/Tools/jEdit/src/proofdocument/ProofDocument.scala --- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Mon Apr 20 20:28:45 2009 +0200 +++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Wed Apr 22 17:35:49 2009 +0200 @@ -75,16 +75,25 @@ val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed) // update indices start = end.foldLeft (start) ((s, t) => s + (t -> (s(t) + change.added.length - change.removed))) - start = removed.foldLeft (start) ((s, t) => s - t) val split_begin = removed.takeWhile(start(_) < change.start). - map (t => new Token(t.content.substring(0, change.start - start(t)), - t.kind)) + map (t => { + val split_tok = new Token(t.content.substring(0, change.start - start(t)), t.kind) + start += (split_tok -> start(t)) + split_tok + }) + val split_end = removed.dropWhile(stop(_) < change.start + change.removed). - map (t => new Token(t.content.substring(change.start + change.removed - start(t)), - t.kind)) + map (t => { + val split_tok = new Token(t.content.substring(change.start + change.removed - start(t)), + t.kind) + start += (split_tok -> start(t)) + split_tok + }) // update indices - start = split_end.foldLeft (start) ((s, t) => s + (t -> (change.start + change.added.length))) + start = removed.foldLeft (start) ((s, t) => s - t) + start = split_end.foldLeft (start) ((s, t) => + s + (t -> (change.start + change.added.length))) val ins = new Token(change.added, Token.Kind.OTHER) start += (ins -> change.start) @@ -121,77 +130,75 @@ } 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, - removed, old_suffix.firstOption, - new_token_list, + new_tokenset, start) } /** command view **/ def find_command_at(pos: Int): Command = { - for (cmd <- commands) { if (pos < cmd.stop) return cmd } + 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], - removed_tokens: List[Token], after_change: Option[Token], - new_token_list: List[Token], + new_tokenset: LinearSet[Token], new_token_start: Map[Token, Int]): (ProofDocument, StructureChange) = { - val commands_list = List[Command]() ++ commands - - // calculate removed commands - val first_removed = removed_tokens.firstOption + 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 (begin, remaining) = - first_removed match { - case None => (Nil, commands_list) - case Some(fr) => commands_list.break(_.tokens.contains(fr)) - } - val (removed_commands, end) = - after_change match { - case None => (remaining, Nil) - case Some(ac) => remaining.break(_.tokens.contains(ac)) - } + 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 removed_commands = commands.dropWhile(Some(_) != cmd_first_changed). + takeWhile(Some(_) != cmd_after_change) + + // calculate inserted commands def tokens_to_commands(tokens: List[Token]): List[Command]= { tokens match { case Nil => Nil case t::ts => val (cmd,rest) = ts.span(_.kind != Token.Kind.COMMAND_START) - new Command(t::cmd) :: tokens_to_commands (rest) + new Command(t::cmd, new_token_start) :: tokens_to_commands (rest) } } - // calculate inserted commands - val new_commands = tokens_to_commands(new_token_list) - val new_tokenset = (LinearSet() ++ new_token_list).asInstanceOf[LinearSet[Token]] - val new_commandset = (LinearSet() ++ (new_commands)).asInstanceOf[LinearSet[Command]] - // drop known commands from the beginning - val first_changed = before_change match { - case None => new_tokenset.first_elem - case Some(bc) => new_tokenset.next(bc) - } - val changed_commands = first_changed match { - case None => Nil - case Some(fc) => new_commands.dropWhile(!_.tokens.contains(fc)) - } - val inserted_commands = after_change match { - case None => changed_commands - case Some(ac) => changed_commands.takeWhile(!_.tokens.contains(ac)) - } - val change = new StructureChange(new_commands.find(_.tokens.contains(before_change)), - inserted_commands, removed_commands) + 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 rescanning_tokens = split_begin_tokens ::: inserted_tokens ::: split_end_tokens + val inserted_commands = tokens_to_commands(rescanning_tokens) + + val change = new StructureChange(cmd_before_change, inserted_commands, removed_commands.toList) // build new document - var new_commands = commands - while(new_commands.next()) + val new_commandset = commands.delete_between(cmd_before_change, cmd_after_change). + insert_after(cmd_before_change, inserted_commands) + val doc = new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset, active, is_command_keyword) return (doc, change) diff -r d013be0adb66 -r 7dc6c231da40 src/Tools/jEdit/src/proofdocument/Token.scala --- a/src/Tools/jEdit/src/proofdocument/Token.scala Mon Apr 20 20:28:45 2009 +0200 +++ b/src/Tools/jEdit/src/proofdocument/Token.scala Wed Apr 22 17:35:49 2009 +0200 @@ -38,5 +38,5 @@ class Token(val content: String, val kind: Token.Kind.Value) { val length = content.length - override def toString = content + "(" + kind + ")" + override def toString = content } diff -r d013be0adb66 -r 7dc6c231da40 src/Tools/jEdit/src/prover/Command.scala --- a/src/Tools/jEdit/src/prover/Command.scala Mon Apr 20 20:28:45 2009 +0200 +++ b/src/Tools/jEdit/src/prover/Command.scala Wed Apr 22 17:35:49 2009 +0200 @@ -29,7 +29,7 @@ } -class Command(val tokens: List[Token]) +class Command(val tokens: List[Token], val starts: Map[Token, Int]) { val id = Isabelle.plugin.id() @@ -38,10 +38,10 @@ override def toString = name val name = tokens.head.content - val content:String = Token.string_from_tokens(tokens.takeWhile(_.kind != Token.Kind.COMMENT)) + val content:String = Token.string_from_tokens(tokens.takeWhile(_.kind != Token.Kind.COMMENT), starts) - def start = tokens.first.start - def stop = tokens.last.stop + def start(doc: ProofDocument) = doc.token_start(tokens.first) + def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length /* command status */ @@ -80,10 +80,14 @@ /* markup */ val root_node = - new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content) + new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, id, Markup.COMMAND_SPAN, content) - def node_from(kind: String, begin: Int, end: Int) = { - val markup_content = content.substring(begin, end) - new MarkupNode(this, begin, end, id, kind, markup_content) + def add_markup(kind: String, begin: Int, end: Int) = { + val markup_content = if (end <= content.length) content.substring(begin, end) + else { + System.err.println (root_node.stop, content, content.length, end) + "wrong indices?" + } + root_node insert new MarkupNode(this, begin, end, id, kind, markup_content) } } diff -r d013be0adb66 -r 7dc6c231da40 src/Tools/jEdit/src/prover/MarkupNode.scala --- a/src/Tools/jEdit/src/prover/MarkupNode.scala Mon Apr 20 20:28:45 2009 +0200 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Wed Apr 22 17:35:49 2009 +0200 @@ -6,6 +6,8 @@ package isabelle.prover +import isabelle.proofdocument.ProofDocument + import sidekick.IAsset import javax.swing._ import javax.swing.text.Position @@ -13,10 +15,10 @@ object MarkupNode { - def markup2default_node(node : MarkupNode) : DefaultMutableTreeNode = { + def markup2default_node(node: MarkupNode, cmd: Command, doc: ProofDocument) : DefaultMutableTreeNode = { implicit def int2pos(offset: Int): Position = - new Position { def getOffset = offset } + new Position { def getOffset = offset; override def toString = offset.toString} object RelativeAsset extends IAsset { override def getIcon : Icon = null @@ -25,10 +27,10 @@ override def getName : String = node.id override def setName (name : String) = () override def setStart(start : Position) = () - override def getStart : Position = node.abs_start + override def getStart : Position = node.abs_start(doc) override def setEnd(end : Position) = () - override def getEnd : Position = node.abs_stop - override def toString = node.id + ": " + node.kind + "[" + node.start + " - " + node.stop + "]" + override def getEnd : Position = node.abs_stop(doc) + override def toString = node.id + ": " + node.kind + "[" + getStart + " - " + getEnd + "]" } new DefaultMutableTreeNode(RelativeAsset) @@ -38,40 +40,27 @@ class MarkupNode (val base : Command, val start : Int, val stop : Int, val id : String, val kind : String, val desc : String) { - val swing_node : DefaultMutableTreeNode = MarkupNode.markup2default_node (this) + def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = { + val node = MarkupNode.markup2default_node (this, base, doc) + for (c <- children) node add c.swing_node(doc) + node + } + + def abs_start(doc: ProofDocument) = base.start(doc) + start + def abs_stop(doc: ProofDocument) = base.start(doc) + stop var parent : MarkupNode = null def orphan = parent == null - def length = stop - start - def abs_start = base.start + start - def abs_stop = base.start + stop - - private var children_cell : List[MarkupNode] = Nil - //track changes in swing_node - def children = children_cell - def children_= (cs : List[MarkupNode]) = { - swing_node.removeAllChildren - for (c <- cs) swing_node add c.swing_node - children_cell = cs - } + var children : List[MarkupNode] = Nil private def add(child : MarkupNode) { child parent = this - children_cell = (child :: children) sort ((a, b) => a.start < b.start) - - swing_node add child.swing_node + children = (child :: children) sort ((a, b) => a.start < b.start) } private def remove(nodes : List[MarkupNode]) { - children_cell = children diff nodes - - for (node <- nodes) try { - swing_node remove node.swing_node - } catch { case e : IllegalArgumentException => - System.err.println(e.toString) - case e => throw e - } + children = children diff nodes } def dfs : List[MarkupNode] = { diff -r d013be0adb66 -r 7dc6c231da40 src/Tools/jEdit/src/prover/Prover.scala --- a/src/Tools/jEdit/src/prover/Prover.scala Mon Apr 20 20:28:45 2009 +0200 +++ b/src/Tools/jEdit/src/prover/Prover.scala Wed Apr 22 17:35:49 2009 +0200 @@ -190,7 +190,7 @@ // inner syntax: id from props else command if (cmd != null) { - cmd.root_node.insert(cmd.node_from(kind, begin, end)) + cmd.add_markup(kind, begin, end) command_change(cmd) } case _ => @@ -249,7 +249,7 @@ for (cmd <- changes.removed_commands) yield { commands -= cmd.id if (cmd.state_id != null) states -= cmd.state_id - (document.commands.prev(cmd).map(_.id).getOrElse(document_id0)) -> None + changes.before_change.map(_.id).getOrElse(document_id0) -> None } val inserts = for (cmd <- changes.added_commands) yield { diff -r d013be0adb66 -r 7dc6c231da40 src/Tools/jEdit/src/utils/LinearSet.scala --- a/src/Tools/jEdit/src/utils/LinearSet.scala Mon Apr 20 20:28:45 2009 +0200 +++ b/src/Tools/jEdit/src/utils/LinearSet.scala Wed Apr 22 17:35:49 2009 +0200 @@ -43,7 +43,7 @@ def contains(elem: A): Boolean = !isEmpty && (last_elem.get == elem || body.isDefinedAt(elem)) - def insert_after(hook: Option[A], elem: A): LinearSet[A] = + private def _insert_after(hook: Option[A], elem: A): LinearSet[A] = if (contains(elem)) throw new LinearSet.Duplicate(elem.toString) else hook match { case Some(hook) => @@ -55,8 +55,11 @@ if (isEmpty) LinearSet.make(Some(elem), Some(elem), Map.empty) else LinearSet.make(Some(elem), last_elem, body + (elem -> first_elem.get)) } - - def +(elem: A): LinearSet[A] = insert_after(last_elem, elem) + + def insert_after(hook: Option[A], elems: Seq[A]): LinearSet[A] = + elems.reverse.foldLeft (this) ((ls, elem) => ls._insert_after(hook, elem)) + + def +(elem: A): LinearSet[A] = _insert_after(last_elem, elem) def delete_after(elem: Option[A]): LinearSet[A] = elem match { @@ -70,7 +73,18 @@ else if (size == 1) empty else LinearSet.make(Some(body(first_elem.get)), last_elem, body - first_elem.get) } - + + def delete_between(from: Option[A], to: Option[A]): LinearSet[A] = { + if(!first_elem.isDefined) this + else { + val next = if (from == last_elem) None + else if (from == None) first_elem + else from.map(body(_)) + if (next == to) this + else delete_after(from).delete_between(from, to) + } + } + def -(elem: A): LinearSet[A] = if (!contains(elem)) throw new LinearSet.Undefined(elem.toString) else delete_after(body find (p => p._2 == elem) map (p => p._1))