maintain name of *the* enclosing node as part of command -- avoid full document traversal;
authorwenzelm
Wed Aug 31 15:41:22 2011 +0200 (2011-08-31)
changeset 44607274eff0ea12e
parent 44606 b625650aa2db
child 44608 76c2e3ddc183
maintain name of *the* enclosing node as part of command -- avoid full document traversal;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/isabelle_hyperlinks.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Wed Aug 31 14:39:41 2011 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Wed Aug 31 15:41:22 2011 +0200
     1.3 @@ -80,10 +80,10 @@
     1.4    /* dummy commands */
     1.5  
     1.6    def unparsed(source: String): Command =
     1.7 -    new Command(Document.no_id, List(Token(Token.Kind.UNPARSED, source)))
     1.8 +    new Command(Document.no_id, "", List(Token(Token.Kind.UNPARSED, source)))
     1.9  
    1.10 -  def span(toks: List[Token]): Command =
    1.11 -    new Command(Document.no_id, toks)
    1.12 +  def span(node_name: String, toks: List[Token]): Command =
    1.13 +    new Command(Document.no_id, node_name, toks)
    1.14  
    1.15  
    1.16    /* perspective */
    1.17 @@ -110,6 +110,7 @@
    1.18  
    1.19  class Command(
    1.20      val id: Document.Command_ID,
    1.21 +    val node_name: String,
    1.22      val span: List[Token])
    1.23  {
    1.24    /* classification */
     2.1 --- a/src/Pure/PIDE/document.scala	Wed Aug 31 14:39:41 2011 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Wed Aug 31 15:41:22 2011 +0200
     2.3 @@ -271,13 +271,12 @@
     2.4  
     2.5      def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id)
     2.6  
     2.7 -    def find_command(version: Version, id: ID): Option[(String, Node, Command)] =
     2.8 +    def find_command(version: Version, id: ID): Option[(Node, Command)] =
     2.9        commands.get(id) orElse execs.get(id) match {
    2.10          case None => None
    2.11          case Some(st) =>
    2.12            val command = st.command
    2.13 -          version.nodes.find({ case (_, node) => node.commands(command) })
    2.14 -            .map({ case (name, node) => (name, node, command) })
    2.15 +          version.nodes.get(command.node_name).map((_, command))
    2.16        }
    2.17  
    2.18      def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
     3.1 --- a/src/Pure/Thy/thy_syntax.scala	Wed Aug 31 14:39:41 2011 +0200
     3.2 +++ b/src/Pure/Thy/thy_syntax.scala	Wed Aug 31 15:41:22 2011 +0200
     3.3 @@ -27,7 +27,8 @@
     3.4        def length: Int = command.length
     3.5      }
     3.6  
     3.7 -    def parse(syntax: Outer_Syntax, root_name: String, text: CharSequence): Entry =
     3.8 +    def parse(syntax: Outer_Syntax, node_name: String, root_name: String, text: CharSequence)
     3.9 +      : Entry =
    3.10      {
    3.11        /* stack operations */
    3.12  
    3.13 @@ -67,7 +68,7 @@
    3.14        /* result structure */
    3.15  
    3.16        val spans = parse_spans(syntax.scan(text))
    3.17 -      spans.foreach(span => add(Command.span(span)))
    3.18 +      spans.foreach(span => add(Command.span(node_name, span)))
    3.19        result()
    3.20      }
    3.21    }
    3.22 @@ -186,7 +187,8 @@
    3.23  
    3.24      /* phase 2: recover command spans */
    3.25  
    3.26 -    @tailrec def recover_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
    3.27 +    @tailrec def recover_spans(node_name: String, commands: Linear_Set[Command])
    3.28 +      : Linear_Set[Command] =
    3.29      {
    3.30        commands.iterator.find(cmd => !cmd.is_defined) match {
    3.31          case Some(first_unparsed) =>
    3.32 @@ -212,10 +214,10 @@
    3.33                (Some(last), spans1.take(spans1.length - 1))
    3.34              else (commands.next(last), spans1)
    3.35  
    3.36 -          val inserted = spans2.map(span => new Command(Document.new_id(), span))
    3.37 +          val inserted = spans2.map(span => new Command(Document.new_id(), node_name, span))
    3.38            val new_commands =
    3.39              commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
    3.40 -          recover_spans(new_commands)
    3.41 +          recover_spans(node_name, new_commands)
    3.42  
    3.43          case None => commands
    3.44        }
    3.45 @@ -237,7 +239,7 @@
    3.46            val node = nodes(name)
    3.47            val commands0 = node.commands
    3.48            val commands1 = edit_text(text_edits, commands0)
    3.49 -          val commands2 = recover_spans(commands1)   // FIXME somewhat slow
    3.50 +          val commands2 = recover_spans(name, commands1)   // FIXME somewhat slow
    3.51  
    3.52            val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
    3.53            val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
     4.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Wed Aug 31 14:39:41 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Wed Aug 31 15:41:22 2011 +0200
     4.3 @@ -74,10 +74,10 @@
     4.4                      (props, props) match {
     4.5                        case (Position.Id(def_id), Position.Offset(def_offset)) =>
     4.6                          snapshot.state.find_command(snapshot.version, def_id) match {
     4.7 -                          case Some((def_name, def_node, def_cmd)) =>
     4.8 +                          case Some((def_node, def_cmd)) =>
     4.9                              def_node.command_start(def_cmd) match {
    4.10                                case Some(def_cmd_start) =>
    4.11 -                                new Internal_Hyperlink(def_name, begin, end, line,
    4.12 +                                new Internal_Hyperlink(def_cmd.node_name, begin, end, line,
    4.13                                    def_cmd_start + def_cmd.decode(def_offset))
    4.14                                case None => null
    4.15                              }
     5.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Aug 31 14:39:41 2011 +0200
     5.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Aug 31 15:41:22 2011 +0200
     5.3 @@ -138,7 +138,7 @@
     5.4        }
     5.5  
     5.6      val text = Isabelle.buffer_text(model.buffer)
     5.7 -    val structure = Structure.parse(syntax, "theory " + model.thy_name, text)
     5.8 +    val structure = Structure.parse(syntax, model.node_name, "theory " + model.thy_name, text)
     5.9  
    5.10      make_tree(0, structure) foreach (node => data.root.add(node))
    5.11    }