--- a/src/Pure/Thy/thy_syntax.scala Fri Aug 10 13:15:00 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Fri Aug 10 13:33:07 2012 +0200
@@ -194,7 +194,7 @@
}
- /* phase 2: recover command spans */
+ /* phase 2a: reparse range of command spans */
@tailrec private def chop_common(
cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
@@ -203,70 +203,95 @@
case _ => (cmds, spans)
}
- private def trim_common(
- cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
+ private def reparse_spans(
+ syntax: Outer_Syntax,
+ name: Document.Node.Name,
+ commands: Linear_Set[Command],
+ first: Command, last: Command): Linear_Set[Command] =
{
- val (cmds1, spans1) = chop_common(cmds, spans)
+ val cmds0 = commands.iterator(first, last).toList
+ val spans0 = parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString))
+
+ val (cmds1, spans1) = chop_common(cmds0, spans0)
+
val (rev_cmds2, rev_spans2) = chop_common(cmds1.reverse, spans1.reverse)
- (rev_cmds2.reverse, rev_spans2.reverse)
+ val cmds2 = rev_cmds2.reverse
+ val spans2 = rev_spans2.reverse
+
+ cmds2 match {
+ case Nil =>
+ assert(spans2.isEmpty)
+ commands
+ case cmd :: _ =>
+ val hook = commands.prev(cmd)
+ val inserted = spans2.map(span => Command(Document.new_id(), name, span))
+ (commands /: cmds2)(_ - _).append_after(hook, inserted)
+ }
}
+
+ /* phase 2b: recover command spans after edits */
+
private def recover_spans(
syntax: Outer_Syntax,
- node_name: Document.Node.Name,
+ name: Document.Node.Name,
perspective: Command.Perspective,
- old_commands: Linear_Set[Command]): Linear_Set[Command] =
+ commands: Linear_Set[Command]): Linear_Set[Command] =
{
- val visible = perspective.commands.iterator.filter(_.is_defined).toSet
+ val visible = perspective.commands.toSet
- def next_invisible_command(commands: Linear_Set[Command], from: Command): Command =
- commands.iterator(from).dropWhile(cmd => !cmd.is_command || visible(cmd))
- .find(_.is_command) getOrElse commands.last
-
- @tailrec def recover(commands: Linear_Set[Command]): Linear_Set[Command] =
- commands.iterator.find(cmd => !cmd.is_defined) match {
- case Some(first_undefined) =>
- val first = next_invisible_command(commands.reverse, first_undefined)
- val last = next_invisible_command(commands, first_undefined)
+ def next_invisible_command(cmds: Linear_Set[Command], from: Command): Command =
+ cmds.iterator(from).dropWhile(cmd => !cmd.is_command || visible(cmd))
+ .find(_.is_command) getOrElse cmds.last
- val cmds0 = commands.iterator(first, last).toList
- val spans0 = parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString))
-
- val (cmds, spans) = trim_common(cmds0, spans0)
- val new_commands =
- cmds match {
- case Nil =>
- assert(spans.isEmpty)
- commands
- case cmd :: _ =>
- val hook = commands.prev(cmd)
- val inserted = spans.map(span => Command(Document.new_id(), node_name, span))
- (commands /: cmds)(_ - _).append_after(hook, inserted)
- }
- recover(new_commands)
-
- case None => commands
+ @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] =
+ cmds.find(_.is_unparsed) match {
+ case Some(first_unparsed) =>
+ val first = next_invisible_command(cmds.reverse, first_unparsed)
+ val last = next_invisible_command(cmds, first_unparsed)
+ recover(reparse_spans(syntax, name, cmds, first, last))
+ case None => cmds
}
- recover(old_commands)
+ recover(commands)
}
- /* phase 3: full reparsing after syntax change */
+ /* phase 2c: consolidate unfinished spans */
- private def reparse_spans(
+ private def consolidate_spans(
syntax: Outer_Syntax,
- node_name: Document.Node.Name,
+ name: Document.Node.Name,
+ perspective: Command.Perspective,
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)): _*)
+ if (perspective.commands.isEmpty) commands
+ else {
+ commands.find(_.is_unfinished) match {
+ case Some(first_unfinished) =>
+ val visible = perspective.commands.toSet
+ commands.reverse.find(visible) match {
+ case Some(last_visible) =>
+ reparse_spans(syntax, name, commands, first_unfinished, last_visible)
+ case None => commands
+ }
+ case None => commands
+ }
+ }
}
/* main phase */
+ private def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command])
+ : List[(Option[Command], Option[Command])] =
+ {
+ val removed = old_cmds.iterator.filter(!new_cmds.contains(_)).toList
+ val inserted = new_cmds.iterator.filter(!old_cmds.contains(_)).toList
+
+ removed.reverse.map(cmd => (old_cmds.prev(cmd), None)) :::
+ inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd)))
+ }
+
def text_edits(
base_syntax: Outer_Syntax,
previous: Document.Version,
@@ -286,21 +311,16 @@
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, node.perspective, commands1) // FIXME somewhat slow
val commands3 =
- if (reparse_set.contains(name)) reparse_spans(syntax, name, commands2) // slow
+ if (reparse_set.contains(name) && !commands2.isEmpty)
+ reparse_spans(syntax, name, commands2, commands2.head, commands2.last) // FIXME somewhat slow
else commands2
- 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))
+ doc_edits += (name -> Document.Node.Edits(diff_commands(commands0, commands3)))
nodes += (name -> node.update_commands(commands3))
case (name, Document.Node.Deps(_)) =>
@@ -309,10 +329,15 @@
val node = nodes(name)
val perspective = command_perspective(node, text_perspective)
if (!(node.perspective same perspective)) {
+/* FIXME
+ val commands1 = consolidate_spans(syntax, name, perspective, node.commands)
+ doc_edits += (name -> Document.Node.Edits(diff_commands(node.commands, commands1)))
+*/
doc_edits += (name -> Document.Node.Perspective(perspective))
nodes += (name -> node.update_perspective(perspective))
}
}
+
(doc_edits.toList, Document.Version.make(syntax, nodes))
}
}