# HG changeset patch # User wenzelm # Date 1426445329 -3600 # Node ID b5eb7c68883647a5d15812e41c9f22ee81232ddd # Parent 081c57f6b22c170f1d8825116a75a55fc57f34b0 tuned; diff -r 081c57f6b22c -r b5eb7c688836 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Sun Mar 15 19:39:31 2015 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Sun Mar 15 19:48:49 2015 +0100 @@ -189,38 +189,6 @@ } - /* recover command spans after edits */ - - // FIXME somewhat slow - private def recover_spans( - resources: Resources, - syntax: Prover.Syntax, - get_blob: Document.Node.Name => Option[Document.Blob], - can_import: Document.Node.Name => Boolean, - node_name: Document.Node.Name, - header: Document.Node.Header, - perspective: Command.Perspective, - commands: Linear_Set[Command]): Linear_Set[Command] = - { - val visible = perspective.commands.toSet - - def next_invisible_command(cmds: Linear_Set[Command], from: Command): Command = - cmds.iterator(from).dropWhile(cmd => !cmd.is_proper || visible(cmd)) - .find(_.is_proper) getOrElse cmds.last - - @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( - resources, syntax, get_blob, can_import, node_name, header, cmds, first, last)) - case None => cmds - } - recover(commands) - } - - /* main */ def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command]) @@ -241,6 +209,32 @@ reparse_limit: Int, node: Document.Node, edit: Document.Edit_Text): Document.Node = { + /* recover command spans after edits */ + // FIXME somewhat slow + def recover_spans( + name: Document.Node.Name, + header: Document.Node.Header, + perspective: Command.Perspective, + commands: Linear_Set[Command]): Linear_Set[Command] = + { + val is_visible = perspective.commands.toSet + + def next_invisible(cmds: Linear_Set[Command], from: Command): Command = + cmds.iterator(from).dropWhile(cmd => !cmd.is_proper || is_visible(cmd)) + .find(_.is_proper) getOrElse cmds.last + + @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] = + cmds.find(_.is_unparsed) match { + case Some(first_unparsed) => + val first = next_invisible(cmds.reverse, first_unparsed) + val last = next_invisible(cmds, first_unparsed) + recover( + reparse_spans(resources, syntax, get_blob, can_import, name, header, cmds, first, last)) + case None => cmds + } + recover(commands) + } + edit match { case (_, Document.Node.Clear()) => node.clear @@ -250,9 +244,7 @@ if (name.is_theory) { val commands0 = node.commands val commands1 = edit_text(text_edits, commands0) - val commands2 = - recover_spans(resources, syntax, get_blob, can_import, name, - node.header, node.perspective.visible, commands1) + val commands2 = recover_spans(name, node.header, node.perspective.visible, commands1) node.update_commands(commands2) } else node