--- a/src/Tools/jEdit/src/jedit/document_model.scala Sun Jan 10 21:08:23 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Sun Jan 10 21:14:44 2010 +0100
@@ -84,7 +84,7 @@
def lines_of_command(doc: Document, cmd: Command): (Int, Int) =
{
- val start = cmd.start(doc)
+ val start = doc.command_start(cmd).get // FIXME total?
val stop = start + cmd.length
(buffer.getLineOfOffset(to_current(doc, start)),
buffer.getLineOfOffset(to_current(doc, stop)))
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Sun Jan 10 21:08:23 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Sun Jan 10 21:14:44 2010 +0100
@@ -56,8 +56,12 @@
case Command.RefInfo(_, _, Some(id), Some(offset)) =>
Isabelle.session.lookup_entity(id) match {
case Some(ref_cmd: Command) =>
- new Internal_Hyperlink(begin, end, line,
- model.to_current(document, ref_cmd.start(document) + offset - 1))
+ document.command_start(ref_cmd) match {
+ case Some(ref_cmd_start) =>
+ new Internal_Hyperlink(begin, end, line,
+ model.to_current(document, ref_cmd_start + offset - 1))
+ case None => null // FIXME external ref
+ }
case _ => null
}
case _ => null
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Sun Jan 10 21:08:23 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Sun Jan 10 21:14:44 2010 +0100
@@ -44,11 +44,10 @@
Swing_Thread.now { Document_Model(buffer) } match {
case Some(model) =>
val document = model.recent_document()
- for (command <- document.commands if !stopped) {
+ for ((command, command_start) <- document.command_range(0) if !stopped) {
root.add(document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
{
val content = command.content(node.start, node.stop)
- val command_start = command.start(document)
val id = command.id
new DefaultMutableTreeNode(new IAsset {
--- a/src/Tools/jEdit/src/proofdocument/command.scala Sun Jan 10 21:08:23 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/command.scala Sun Jan 10 21:14:44 2010 +0100
@@ -53,8 +53,6 @@
def length: Int = content.length
- def start(doc: Document) = doc.token_start(tokens.first)
-
// FIXME eliminate
def contains(p: Token) = tokens.contains(p)