--- 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)
--- 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
}
--- 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 + "]"
})
--- 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)
}
--- 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
}
}