# HG changeset patch # User wenzelm # Date 1344604485 -7200 # Node ID 393a37003851a65b3f3f00a69f046e9fc46d624a # Parent c2c1e594453615f1ffb7fd2670e01f60f15e323e apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.; expand Clear edit before sending to prover; at most one full reparse of each node; diff -r c2c1e5944536 -r 393a37003851 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Aug 10 13:33:07 2012 +0200 +++ b/src/Pure/PIDE/document.ML Fri Aug 10 15:14:45 2012 +0200 @@ -17,7 +17,7 @@ val print_id: id -> string type node_header = string * Thy_Header.header * string list datatype node_edit = - Clear | + Clear | (* FIXME unused !? *) Edits of (command_id option * command_id option) list | Deps of node_header | Perspective of command_id list diff -r c2c1e5944536 -r 393a37003851 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Fri Aug 10 13:33:07 2012 +0200 +++ b/src/Pure/PIDE/protocol.ML Fri Aug 10 15:14:45 2012 +0200 @@ -33,7 +33,7 @@ let open XML.Decode in list (pair string (variant - [fn ([], []) => Document.Clear, + [fn ([], []) => Document.Clear, (* FIXME unused !? *) fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), fn ([], a) => let diff -r c2c1e5944536 -r 393a37003851 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Fri Aug 10 13:33:07 2012 +0200 +++ b/src/Pure/PIDE/protocol.scala Fri Aug 10 15:14:45 2012 +0200 @@ -213,7 +213,7 @@ def encode_edit(name: Document.Node.Name) : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] = variant(List( - { case Document.Node.Clear() => (Nil, Nil) }, + { case Document.Node.Clear() => (Nil, Nil) }, // FIXME unused !? { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, { case Document.Node.Deps(header) => val dir = Isabelle_System.posix_path(name.dir) diff -r c2c1e5944536 -r 393a37003851 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Fri Aug 10 13:33:07 2012 +0200 +++ b/src/Pure/System/session.scala Fri Aug 10 15:14:45 2012 +0200 @@ -453,7 +453,7 @@ header: Document.Node.Header, perspective: Text.Perspective, text: String) { edit(List(header_edit(name, header), - name -> Document.Node.Clear(), // FIXME diff wrt. existing node + name -> Document.Node.Clear(), name -> Document.Node.Edits(List(Text.Edit.insert(0, text))), name -> Document.Node.Perspective(perspective))) } diff -r c2c1e5944536 -r 393a37003851 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Fri Aug 10 13:33:07 2012 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Fri Aug 10 15:14:45 2012 +0200 @@ -165,7 +165,7 @@ /** text edits **/ - /* phase 1: edit individual command source */ + /* edit individual command source */ @tailrec private def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command]) : Linear_Set[Command] = @@ -194,7 +194,7 @@ } - /* phase 2a: reparse range of command spans */ + /* reparse range of command spans */ @tailrec private def chop_common( cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) = @@ -230,8 +230,9 @@ } - /* phase 2b: recover command spans after edits */ + /* recover command spans after edits */ + // FIXME somewhat slow private def recover_spans( syntax: Outer_Syntax, name: Document.Node.Name, @@ -256,7 +257,7 @@ } - /* phase 2c: consolidate unfinished spans */ + /* consolidate unfinished spans */ private def consolidate_spans( syntax: Outer_Syntax, @@ -280,7 +281,7 @@ } - /* main phase */ + /* main */ private def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command]) : List[(Option[Command], Option[Command])] = @@ -292,6 +293,29 @@ inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd))) } + private def text_edit(syntax: Outer_Syntax, + node: Document.Node, edit: Document.Edit_Text): Document.Node = + { + edit match { + case (_, Document.Node.Clear()) => node.clear + + case (name, Document.Node.Edits(text_edits)) => + val commands0 = node.commands + val commands1 = edit_text(text_edits, commands0) + val commands2 = recover_spans(syntax, name, node.perspective, commands1) + node.update_commands(commands2) + + case (_, Document.Node.Deps(_)) => node + + case (name, Document.Node.Perspective(text_perspective)) => + val perspective = command_perspective(node, text_perspective) + if (node.perspective same perspective) node + else + node.update_perspective(perspective) + .update_commands(consolidate_spans(syntax, name, perspective, node.commands)) + } + } + def text_edits( base_syntax: Outer_Syntax, previous: Document.Version, @@ -304,38 +328,27 @@ var nodes = nodes0 val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0 - (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 (name, Document.Node.Edits(text_edits)) => - val node = nodes(name) + val node_edits = + (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1) + .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]] // FIXME ??? - 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) && !commands2.isEmpty) - reparse_spans(syntax, name, commands2, commands2.head, commands2.last) // FIXME somewhat slow - else commands2 + node_edits foreach { + case (name, edits) => + val node = nodes(name) + val commands = node.commands - doc_edits += (name -> Document.Node.Edits(diff_commands(commands0, commands3))) - nodes += (name -> node.update_commands(commands3)) - - case (name, Document.Node.Deps(_)) => + val node1 = + if (reparse_set(name) && !commands.isEmpty) + node.update_commands(reparse_spans(syntax, name, commands, commands.head, commands.last)) + else node + val node2 = (node1 /: edits)(text_edit(syntax, _, _)) - case (name, Document.Node.Perspective(text_perspective)) => - 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)) - } + if (!(node.perspective same node2.perspective)) + doc_edits += (name -> Document.Node.Perspective(node2.perspective)) + + doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands))) + + nodes += (name -> node2) } (doc_edits.toList, Document.Version.make(syntax, nodes))