# HG changeset patch
# User wenzelm
# Date 1263154484 -3600
# Node ID ad486bd8abf3c7b9750726bc6c2d81550303b24f
# Parent  d3cffc4241f2bc23fac71cc1f09cc9577d8f89d2
further tuning of command_start;

diff -r d3cffc4241f2 -r ad486bd8abf3 src/Tools/jEdit/src/jedit/document_model.scala
--- 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)))
diff -r d3cffc4241f2 -r ad486bd8abf3 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- 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
diff -r d3cffc4241f2 -r ad486bd8abf3 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- 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 {
diff -r d3cffc4241f2 -r ad486bd8abf3 src/Tools/jEdit/src/proofdocument/command.scala
--- 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)