# HG changeset patch # User wenzelm # Date 1331829954 -3600 # Node ID acc8ebf980cae9a8774bff19fbb8cbe53f092e79 # Parent 26007caf6e9c5f8136a4d05c1d6788282826a2eb more explicit header_edits before main text_edits; handle reparses caused by syntax update; diff -r 26007caf6e9c -r acc8ebf980ca src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Thu Mar 15 17:40:26 2012 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Thu Mar 15 17:45:54 2012 +0100 @@ -142,148 +142,182 @@ + /** header edits: structure and outer syntax **/ + + private def header_edits( + base_syntax: Outer_Syntax, + previous: Document.Version, + edits: List[Document.Edit_Text]) + : (Outer_Syntax, List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) = + { + var rebuild_syntax = previous.is_init + var nodes = previous.nodes + val doc_edits = new mutable.ListBuffer[Document.Edit_Command] + + edits foreach { + case (name, Document.Node.Header(header)) => + val node = nodes(name) + val update_header = + (node.header, header) match { + case (Exn.Res(deps0), Exn.Res(deps)) => deps0 != deps + case _ => true + } + if (update_header) { + val node1 = node.update_header(header) + rebuild_syntax = rebuild_syntax || (node.keywords != node1.keywords) + nodes += (name -> node1) + doc_edits += (name -> Document.Node.Header(header)) + } + case _ => + } + + val syntax = + if (rebuild_syntax) + (base_syntax /: nodes.entries)({ case (syn, (_, node)) => (syn /: node.keywords)(_ + _) }) + else previous.syntax + + val reparse = + if (rebuild_syntax) nodes.descendants(doc_edits.iterator.map(_._1).toList) + else Nil + + (syntax, reparse, nodes, doc_edits.toList) + } + + + /** text edits **/ + /* phase 1: edit individual command source */ + + @tailrec private def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command]) + : Linear_Set[Command] = + { + eds match { + case e :: es => + Document.Node.command_starts(commands.iterator).find { + case (cmd, cmd_start) => + e.can_edit(cmd.source, cmd_start) || + e.is_insert && e.start == cmd_start + cmd.length + } match { + case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) => + val (rest, text) = e.edit(cmd.source, cmd_start) + val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd + edit_text(rest.toList ::: es, new_commands) + + case Some((cmd, cmd_start)) => + edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text))) + + case None => + require(e.is_insert && e.start == 0) + edit_text(es, commands.insert_after(None, Command.unparsed(e.text))) + } + case Nil => commands + } + } + + + /* phase 2: recover command spans */ + + @tailrec private def recover_spans( + syntax: Outer_Syntax, + node_name: Document.Node.Name, + commands: Linear_Set[Command]): Linear_Set[Command] = + { + commands.iterator.find(cmd => !cmd.is_defined) match { + case Some(first_unparsed) => + val first = + commands.reverse_iterator(first_unparsed). + dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.head + val last = + commands.iterator(first_unparsed). + dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last + val range = + commands.iterator(first).takeWhile(_ != last).toList ::: List(last) + + val spans0 = parse_spans(syntax.scan(range.map(_.source).mkString)) + + val (before_edit, spans1) = + if (!spans0.isEmpty && first.is_command && first.span == spans0.head) + (Some(first), spans0.tail) + else (commands.prev(first), spans0) + + val (after_edit, spans2) = + if (!spans1.isEmpty && last.is_command && last.span == spans1.last) + (Some(last), spans1.take(spans1.length - 1)) + else (commands.next(last), spans1) + + val inserted = spans2.map(span => Command(Document.new_id(), node_name, span)) + val new_commands = + commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted) + recover_spans(syntax, node_name, new_commands) + + case None => commands + } + } + + + /* phase 3: full reparsing after syntax change */ + + private def reparse_spans( + syntax: Outer_Syntax, + node_name: Document.Node.Name, + commands: Linear_Set[Command]): Linear_Set[Command] = + { + val cmds = commands.toList + val spans1 = parse_spans(syntax.scan(cmds.map(_.source).mkString)) + if (cmds.map(_.span) == spans1) commands + else Linear_Set(spans1.map(span => Command(Document.new_id(), node_name, span)): _*) + } + + + /* main phase */ + def text_edits( base_syntax: Outer_Syntax, previous: Document.Version, edits: List[Document.Edit_Text]) : (List[Document.Edit_Command], Document.Version) = { - /* phase 1: edit individual command source */ + val (syntax, reparse, nodes0, doc_edits0) = header_edits(base_syntax, previous, edits) + val reparse_set = reparse.toSet + + var nodes = nodes0 + val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0 - @tailrec def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command]) - : Linear_Set[Command] = - { - eds match { - case e :: es => - Document.Node.command_starts(commands.iterator).find { - case (cmd, cmd_start) => - e.can_edit(cmd.source, cmd_start) || - e.is_insert && e.start == cmd_start + cmd.length - } match { - case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) => - val (rest, text) = e.edit(cmd.source, cmd_start) - val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd - edit_text(rest.toList ::: es, new_commands) + (edits ::: reparse.map((_, Document.Node.Edits(Nil)))) foreach { + case (name, Document.Node.Clear()) => + doc_edits += (name -> Document.Node.Clear()) + nodes += (name -> nodes(name).clear) - case Some((cmd, cmd_start)) => - edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text))) - - case None => - require(e.is_insert && e.start == 0) - edit_text(es, commands.insert_after(None, Command.unparsed(e.text))) - } - case Nil => commands - } - } - - - /* phase 2: recover command spans */ + case (name, Document.Node.Edits(text_edits)) => + val node = nodes(name) + val commands0 = node.commands + val commands1 = edit_text(text_edits, commands0) + val commands2 = recover_spans(syntax, name, commands1) // FIXME somewhat slow + val commands3 = + if (reparse_set.contains(name)) reparse_spans(syntax, name, commands2) // slow + else commands2 - @tailrec def recover_spans( - syntax: Outer_Syntax, - node_name: Document.Node.Name, - commands: Linear_Set[Command]): Linear_Set[Command] = - { - commands.iterator.find(cmd => !cmd.is_defined) match { - case Some(first_unparsed) => - val first = - commands.reverse_iterator(first_unparsed). - dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.head - val last = - commands.iterator(first_unparsed). - dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last - val range = - commands.iterator(first).takeWhile(_ != last).toList ::: List(last) + val removed_commands = commands0.iterator.filter(!commands3.contains(_)).toList + val inserted_commands = commands3.iterator.filter(!commands0.contains(_)).toList + + val cmd_edits = + removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) ::: + inserted_commands.map(cmd => (commands3.prev(cmd), Some(cmd))) + + doc_edits += (name -> Document.Node.Edits(cmd_edits)) + nodes += (name -> node.update_commands(commands3)) - val sources = range.flatMap(_.span.map(_.source)) - val spans0 = parse_spans(syntax.scan(sources.mkString)) - - val (before_edit, spans1) = - if (!spans0.isEmpty && first.is_command && first.span == spans0.head) - (Some(first), spans0.tail) - else (commands.prev(first), spans0) + case (name, Document.Node.Header(_)) => - val (after_edit, spans2) = - if (!spans1.isEmpty && last.is_command && last.span == spans1.last) - (Some(last), spans1.take(spans1.length - 1)) - else (commands.next(last), spans1) - - val inserted = spans2.map(span => Command(Document.new_id(), node_name, span)) - val new_commands = - commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted) - recover_spans(syntax, node_name, new_commands) - - case None => commands - } + case (name, Document.Node.Perspective(text_perspective)) => + update_perspective(nodes, name, text_perspective) match { + case (_, None) => + case (perspective, Some(nodes1)) => + doc_edits += (name -> Document.Node.Perspective(perspective)) + nodes = nodes1 + } } - - - /* resulting document edits */ - - { - val doc_edits = new mutable.ListBuffer[Document.Edit_Command] - var nodes = previous.nodes - var rebuild_syntax = previous.is_init - - // structure and syntax - edits foreach { - case (name, Document.Node.Header(header)) => - val node = nodes(name) - val update_header = - (node.header, header) match { - case (Exn.Res(deps0), Exn.Res(deps)) => deps0 != deps - case _ => true - } - if (update_header) { - doc_edits += (name -> Document.Node.Header(header)) - val node1 = node.update_header(header) - nodes += (name -> node1) - rebuild_syntax = rebuild_syntax || (node.keywords != node1.keywords) - } - - case _ => - } - - val syntax = - if (rebuild_syntax) - (base_syntax /: nodes.entries)({ case (syn, (_, node)) => (syn /: node.keywords)(_ + _) }) - else previous.syntax - - // node content - edits foreach { // FIXME observe rebuild_syntax!? - case (name, Document.Node.Clear()) => - doc_edits += (name -> Document.Node.Clear()) - nodes += (name -> nodes(name).clear) - - case (name, Document.Node.Edits(text_edits)) => - val node = nodes(name) - val commands0 = node.commands - val commands1 = edit_text(text_edits, commands0) - val commands2 = recover_spans(syntax, name, commands1) // FIXME somewhat slow - - val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList - val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList - - val cmd_edits = - removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) ::: - inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd))) - - doc_edits += (name -> Document.Node.Edits(cmd_edits)) - nodes += (name -> node.update_commands(commands2)) - - case (name, Document.Node.Header(_)) => - - case (name, Document.Node.Perspective(text_perspective)) => - update_perspective(nodes, name, text_perspective) match { - case (_, None) => - case (perspective, Some(nodes1)) => - doc_edits += (name -> Document.Node.Perspective(perspective)) - nodes = nodes1 - } - } - (doc_edits.toList, Document.Version.make(syntax, nodes)) - } + (doc_edits.toList, Document.Version.make(syntax, nodes)) } }