# HG changeset patch # User wenzelm # Date 1252100622 -7200 # Node ID 504cab625d3e6f2197604cf6ccfd807db35e1963 # Parent ff037c17332a3ce909a8d945df37d915b95cef54 simplified MarkupNode -- independent of Command and ProofDocument; tuned; diff -r ff037c17332a -r 504cab625d3e src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala --- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Fri Sep 04 23:04:20 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Fri Sep 04 23:43:42 2009 +0200 @@ -119,8 +119,9 @@ while (command != null && command.start(document) < from(stop)) { for { markup <- command.highlight_node(document).flatten - abs_stop = to(markup.abs_stop(document)) - abs_start = to(markup.abs_start(document)) + command_start = command.start(document) + abs_start = to(command_start + markup.start) + abs_stop = to(command_start + markup.stop) if (abs_stop > start) if (abs_start < stop) byte = DynamicTokenMarker.choose_byte(markup.info.toString) diff -r ff037c17332a -r 504cab625d3e src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala --- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Fri Sep 04 23:04:20 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Fri Sep 04 23:43:42 2009 +0200 @@ -51,22 +51,23 @@ val theory_view = theory_view_opt.get val document = theory_view.current_document() val offset = theory_view.from_current(document, original_offset) - val cmd = document.find_command_at(offset) - if (cmd != null) { - val ref_o = cmd.ref_at(document, offset - cmd.start(document)) + val command = document.find_command_at(offset) + if (command != null) { + val ref_o = command.ref_at(document, offset - command.start(document)) if (!ref_o.isDefined) null else { val ref = ref_o.get - val start = theory_view.to_current(document, ref.abs_start(document)) - val line = buffer.getLineOfOffset(start) - val end = theory_view.to_current(document, ref.abs_stop(document)) + val command_start = command.start(document) + val begin = theory_view.to_current(document, command_start + ref.start) + val line = buffer.getLineOfOffset(begin) + val end = theory_view.to_current(document, command_start + ref.stop) ref.info match { case RefInfo(Some(ref_file), Some(ref_line), _, _) => - new ExternalHyperlink(start, end, line, ref_file, ref_line) + new ExternalHyperlink(begin, end, line, ref_file, ref_line) case RefInfo(_, _, Some(id), Some(offset)) => prover.get.command(id) match { case Some(ref_cmd) => - new InternalHyperlink(start, end, line, + new InternalHyperlink(begin, end, line, theory_view.to_current(document, ref_cmd.start(document) + offset - 1)) case _ => null } diff -r ff037c17332a -r 504cab625d3e src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala --- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Fri Sep 04 23:04:20 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Fri Sep 04 23:43:42 2009 +0200 @@ -40,11 +40,12 @@ val document = prover_setup.get.theory_view.current_document() for (command <- document.commands if !stopped) { data.root.add(command.markup_root(document). - swing_tree(document)((node: MarkupNode, cmd: Command, doc: ProofDocument) => + swing_tree((node: MarkupNode) => { implicit def int2pos(offset: Int): Position = new Position { def getOffset = offset; override def toString = offset.toString } + val command_start = command.start(document) new DefaultMutableTreeNode(new IAsset { override def getIcon: Icon = null override def getShortString: String = node.content @@ -52,9 +53,9 @@ override def getName: String = node.id override def setName(name: String) = () override def setStart(start: Position) = () - override def getStart: Position = node.abs_start(doc) + override def getStart: Position = command_start + node.start override def setEnd(end: Position) = () - override def getEnd: Position = node.abs_stop(doc) + override def getEnd: Position = command_start + node.stop override def toString = node.id + ": " + node.content + "[" + getStart + " - " + getEnd + "]" }) diff -r ff037c17332a -r 504cab625d3e src/Tools/jEdit/src/prover/Command.scala --- a/src/Tools/jEdit/src/prover/Command.scala Fri Sep 04 23:04:20 2009 +0200 +++ b/src/Tools/jEdit/src/prover/Command.scala Fri Sep 04 23:43:42 2009 +0200 @@ -78,14 +78,14 @@ /* markup */ lazy val empty_root_node = - new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, + new MarkupNode(0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, Nil, id, content, RootInfo()) def markup_node(begin: Int, end: Int, info: MarkupInfo): MarkupNode = { val start = symbol_index.decode(begin) val stop = symbol_index.decode(end) - new MarkupNode(this, start, stop, Nil, id, content.substring(start, stop), info) + new MarkupNode(start, stop, Nil, id, content.substring(start, stop), info) } diff -r ff037c17332a -r 504cab625d3e src/Tools/jEdit/src/prover/MarkupNode.scala --- a/src/Tools/jEdit/src/prover/MarkupNode.scala Fri Sep 04 23:04:20 2009 +0200 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Fri Sep 04 23:43:42 2009 +0200 @@ -24,25 +24,20 @@ } -class MarkupNode(val base: Command, val start: Int, val stop: Int, +class MarkupNode(val start: Int, val stop: Int, val children: List[MarkupNode], val id: String, val content: String, val info: MarkupInfo) { - def swing_tree(doc: ProofDocument) - (make_node: (MarkupNode, Command, ProofDocument) => DefaultMutableTreeNode): - DefaultMutableTreeNode = + def swing_tree(make_node: MarkupNode => DefaultMutableTreeNode): DefaultMutableTreeNode = { - val node = make_node(this, base, doc) - children.foreach(node add _.swing_tree(doc)(make_node)) + val node = make_node(this) + children.foreach(node add _.swing_tree(make_node)) node } - def abs_start(doc: ProofDocument) = base.start(doc) + start - def abs_stop(doc: ProofDocument) = base.start(doc) + stop - def set_children(new_children: List[MarkupNode]): MarkupNode = - new MarkupNode(base, start, stop, new_children, id, content, info) + new MarkupNode(start, stop, new_children, id, content, info) private def add(child: MarkupNode) = // FIXME avoid sort? set_children ((child :: children) sort ((a, b) => a.start < b.start)) @@ -96,13 +91,14 @@ child <- children markups = if (next_x < child.start) { - new MarkupNode(base, next_x, child.start, Nil, id, content, info) :: child.flatten - } else child.flatten + new MarkupNode(next_x, child.start, Nil, id, content, info) :: child.flatten + } + else child.flatten update = (next_x = child.stop) markup <- markups } yield markup if (next_x < stop) - filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, info) + filled_gaps + new MarkupNode(next_x, stop, Nil, id, content, info) else filled_gaps } }