# HG changeset patch
# User wenzelm
# Date 1314798082 -7200
# Node ID 274eff0ea12e5de955f43fdda264685933d4cc28
# Parent  b625650aa2dbff6a9f5ae14f381025cd1ac65b2c
maintain name of *the* enclosing node as part of command -- avoid full document traversal;

diff -r b625650aa2db -r 274eff0ea12e src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Aug 31 14:39:41 2011 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Aug 31 15:41:22 2011 +0200
@@ -80,10 +80,10 @@
   /* dummy commands */
 
   def unparsed(source: String): Command =
-    new Command(Document.no_id, List(Token(Token.Kind.UNPARSED, source)))
+    new Command(Document.no_id, "", List(Token(Token.Kind.UNPARSED, source)))
 
-  def span(toks: List[Token]): Command =
-    new Command(Document.no_id, toks)
+  def span(node_name: String, toks: List[Token]): Command =
+    new Command(Document.no_id, node_name, toks)
 
 
   /* perspective */
@@ -110,6 +110,7 @@
 
 class Command(
     val id: Document.Command_ID,
+    val node_name: String,
     val span: List[Token])
 {
   /* classification */
diff -r b625650aa2db -r 274eff0ea12e src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Aug 31 14:39:41 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Aug 31 15:41:22 2011 +0200
@@ -271,13 +271,12 @@
 
     def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id)
 
-    def find_command(version: Version, id: ID): Option[(String, Node, Command)] =
+    def find_command(version: Version, id: ID): Option[(Node, Command)] =
       commands.get(id) orElse execs.get(id) match {
         case None => None
         case Some(st) =>
           val command = st.command
-          version.nodes.find({ case (_, node) => node.commands(command) })
-            .map({ case (name, node) => (name, node, command) })
+          version.nodes.get(command.node_name).map((_, command))
       }
 
     def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
diff -r b625650aa2db -r 274eff0ea12e src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Aug 31 14:39:41 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Aug 31 15:41:22 2011 +0200
@@ -27,7 +27,8 @@
       def length: Int = command.length
     }
 
-    def parse(syntax: Outer_Syntax, root_name: String, text: CharSequence): Entry =
+    def parse(syntax: Outer_Syntax, node_name: String, root_name: String, text: CharSequence)
+      : Entry =
     {
       /* stack operations */
 
@@ -67,7 +68,7 @@
       /* result structure */
 
       val spans = parse_spans(syntax.scan(text))
-      spans.foreach(span => add(Command.span(span)))
+      spans.foreach(span => add(Command.span(node_name, span)))
       result()
     }
   }
@@ -186,7 +187,8 @@
 
     /* phase 2: recover command spans */
 
-    @tailrec def recover_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
+    @tailrec def recover_spans(node_name: String, commands: Linear_Set[Command])
+      : Linear_Set[Command] =
     {
       commands.iterator.find(cmd => !cmd.is_defined) match {
         case Some(first_unparsed) =>
@@ -212,10 +214,10 @@
               (Some(last), spans1.take(spans1.length - 1))
             else (commands.next(last), spans1)
 
-          val inserted = spans2.map(span => new Command(Document.new_id(), span))
+          val inserted = spans2.map(span => new Command(Document.new_id(), node_name, span))
           val new_commands =
             commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
-          recover_spans(new_commands)
+          recover_spans(node_name, new_commands)
 
         case None => commands
       }
@@ -237,7 +239,7 @@
           val node = nodes(name)
           val commands0 = node.commands
           val commands1 = edit_text(text_edits, commands0)
-          val commands2 = recover_spans(commands1)   // FIXME somewhat slow
+          val commands2 = recover_spans(name, commands1)   // FIXME somewhat slow
 
           val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
           val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
diff -r b625650aa2db -r 274eff0ea12e src/Tools/jEdit/src/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Wed Aug 31 14:39:41 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Wed Aug 31 15:41:22 2011 +0200
@@ -74,10 +74,10 @@
                     (props, props) match {
                       case (Position.Id(def_id), Position.Offset(def_offset)) =>
                         snapshot.state.find_command(snapshot.version, def_id) match {
-                          case Some((def_name, def_node, def_cmd)) =>
+                          case Some((def_node, def_cmd)) =>
                             def_node.command_start(def_cmd) match {
                               case Some(def_cmd_start) =>
-                                new Internal_Hyperlink(def_name, begin, end, line,
+                                new Internal_Hyperlink(def_cmd.node_name, begin, end, line,
                                   def_cmd_start + def_cmd.decode(def_offset))
                               case None => null
                             }
diff -r b625650aa2db -r 274eff0ea12e src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Aug 31 14:39:41 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Aug 31 15:41:22 2011 +0200
@@ -138,7 +138,7 @@
       }
 
     val text = Isabelle.buffer_text(model.buffer)
-    val structure = Structure.parse(syntax, "theory " + model.thy_name, text)
+    val structure = Structure.parse(syntax, model.node_name, "theory " + model.thy_name, text)
 
     make_tree(0, structure) foreach (node => data.root.add(node))
   }