# HG changeset patch # User wenzelm # Date 1384890823 -3600 # Node ID 744ea0025e11d19ebfa00d41a9b474a43a141bc8 # Parent cee77d2e9582821f2bbeb1ad7960831a7ebf7634 clarified Document.Blobs environment vs. actual edits of auxiliary files; more robust handling of vacuous edits; diff -r cee77d2e9582 -r 744ea0025e11 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Nov 19 19:43:26 2013 +0100 +++ b/src/Pure/PIDE/document.scala Tue Nov 19 20:53:43 2013 +0100 @@ -47,6 +47,8 @@ type Edit_Text = Edit[Text.Edit, Text.Perspective] type Edit_Command = Edit[Command.Edit, Command.Perspective] + type Blobs = Map[Node.Name, Bytes] + object Node { val empty: Node = new Node() @@ -125,7 +127,7 @@ case class Edits[A, B](edits: List[A]) extends Edit[A, B] case class Deps[A, B](header: Header) extends Edit[A, B] case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B] - case class Blob[A, B](blob: Bytes) extends Edit[A, B] + case class Blob[A, B]() extends Edit[A, B] type Perspective_Text = Perspective[Text.Edit, Text.Perspective] type Perspective_Command = Perspective[Command.Edit, Command.Perspective] diff -r cee77d2e9582 -r 744ea0025e11 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Tue Nov 19 19:43:26 2013 +0100 +++ b/src/Pure/System/session.scala Tue Nov 19 20:53:43 2013 +0100 @@ -25,7 +25,7 @@ case class Statistics(props: Properties.T) case class Global_Options(options: Options) case object Caret_Focus - case class Raw_Edits(edits: List[Document.Edit_Text]) + case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String) case class Commands_Changed( assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command]) @@ -167,6 +167,7 @@ //{{{ private case class Text_Edits( previous: Future[Document.Version], + doc_blobs: Document.Blobs, text_edits: List[Document.Edit_Text], version_result: Promise[Document.Version]) @@ -177,14 +178,14 @@ receive { case Stop => finished = true; reply(()) - case Text_Edits(previous, text_edits, version_result) => + case Text_Edits(previous, doc_blobs, text_edits, version_result) => val prev = previous.get_finished - val (all_blobs, doc_edits, version) = + val (doc_edits, version) = Timing.timeit("Thy_Load.text_edits", timing) { - thy_load.text_edits(reparse_limit, prev, text_edits) + thy_load.text_edits(reparse_limit, prev, doc_blobs, text_edits) } version_result.fulfill(version) - sender ! Change(all_blobs, doc_edits, prev, version) + sender ! Change(doc_blobs, doc_edits, prev, version) case bad => System.err.println("change_parser: ignoring bad message " + bad) } @@ -250,7 +251,7 @@ private case class Start(args: List[String]) private case class Cancel_Exec(exec_id: Document_ID.Exec) private case class Change( - all_blobs: Map[Document.Node.Name, Bytes], + doc_blobs: Document.Blobs, doc_edits: List[Document.Edit_Command], previous: Document.Version, version: Document.Version) @@ -349,7 +350,7 @@ /* raw edits */ - def handle_raw_edits(edits: List[Document.Edit_Text]) + def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) //{{{ { prover.get.discontinue_execution() @@ -358,8 +359,8 @@ val version = Future.promise[Document.Version] val change = global_state >>> (_.continue_history(previous, edits, version)) - raw_edits.event(Session.Raw_Edits(edits)) - change_parser ! Text_Edits(previous, edits, version) + raw_edits.event(Session.Raw_Edits(doc_blobs, edits)) + change_parser ! Text_Edits(previous, doc_blobs, edits, version) } //}}} @@ -379,7 +380,7 @@ digest <- command.blobs_digests if !global_state().defined_blob(digest) } { - change.all_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match { + change.doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match { case Some(blob) => global_state >> (_.define_blob(digest)) prover.get.define_blob(blob) @@ -523,7 +524,7 @@ case Update_Options(options) if prover.isDefined => if (is_ready) { prover.get.options(options) - handle_raw_edits(Nil) + handle_raw_edits(Map.empty, Nil) } global_options.event(Session.Global_Options(options)) reply(()) @@ -531,8 +532,8 @@ case Cancel_Exec(exec_id) if prover.isDefined => prover.get.cancel_exec(exec_id) - case Session.Raw_Edits(edits) if prover.isDefined => - handle_raw_edits(edits) + case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined => + handle_raw_edits(doc_blobs, edits) reply(()) case Session.Dialog_Result(id, serial, result) if prover.isDefined => @@ -585,8 +586,8 @@ def cancel_exec(exec_id: Document_ID.Exec) { session_actor ! Cancel_Exec(exec_id) } - def update(edits: List[Document.Edit_Text]) - { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(edits) } + def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) + { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(doc_blobs, edits) } def update_options(options: Options) { session_actor !? Update_Options(options) } diff -r cee77d2e9582 -r 744ea0025e11 src/Pure/Thy/thy_load.scala --- a/src/Pure/Thy/thy_load.scala Tue Nov 19 19:43:26 2013 +0100 +++ b/src/Pure/Thy/thy_load.scala Tue Nov 19 20:53:43 2013 +0100 @@ -99,8 +99,11 @@ /* theory text edits */ - def text_edits(reparse_limit: Int, previous: Document.Version, edits: List[Document.Edit_Text]) - : (Map[Document.Node.Name, Bytes], List[Document.Edit_Command], Document.Version) = - Thy_Syntax.text_edits(this, reparse_limit, previous, edits) + def text_edits( + reparse_limit: Int, + previous: Document.Version, + doc_blobs: Document.Blobs, + edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) = + Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits) } diff -r cee77d2e9582 -r 744ea0025e11 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Tue Nov 19 19:43:26 2013 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Tue Nov 19 20:53:43 2013 +0100 @@ -256,14 +256,14 @@ syntax: Outer_Syntax, node_name: Document.Node.Name, span: List[Token], - all_blobs: Map[Document.Node.Name, Bytes]) + doc_blobs: Document.Blobs) : List[Command.Blob] = { span_files(syntax, span).map(file => Exn.capture { val name = Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file))) - all_blobs.get(name) match { + doc_blobs.get(name) match { case Some(blob) => (name, blob.sha1_digest) case None => error("No such file: " + quote(name.toString)) } @@ -286,7 +286,7 @@ private def reparse_spans( thy_load: Thy_Load, syntax: Outer_Syntax, - all_blobs: Map[Document.Node.Name, Bytes], + doc_blobs: Document.Blobs, name: Document.Node.Name, commands: Linear_Set[Command], first: Command, last: Command): Linear_Set[Command] = @@ -294,7 +294,7 @@ val cmds0 = commands.iterator(first, last).toList val spans0 = parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)). - map(span => (resolve_files(thy_load, syntax, name, span, all_blobs), span)) + map(span => (resolve_files(thy_load, syntax, name, span, doc_blobs), span)) val (cmds1, spans1) = chop_common(cmds0, spans0) @@ -321,7 +321,7 @@ private def recover_spans( thy_load: Thy_Load, syntax: Outer_Syntax, - all_blobs: Map[Document.Node.Name, Bytes], + doc_blobs: Document.Blobs, name: Document.Node.Name, perspective: Command.Perspective, commands: Linear_Set[Command]): Linear_Set[Command] = @@ -337,7 +337,7 @@ case Some(first_unparsed) => val first = next_invisible_command(cmds.reverse, first_unparsed) val last = next_invisible_command(cmds, first_unparsed) - recover(reparse_spans(thy_load, syntax, all_blobs, name, cmds, first, last)) + recover(reparse_spans(thy_load, syntax, doc_blobs, name, cmds, first, last)) case None => cmds } recover(commands) @@ -349,7 +349,7 @@ private def consolidate_spans( thy_load: Thy_Load, syntax: Outer_Syntax, - all_blobs: Map[Document.Node.Name, Bytes], + doc_blobs: Document.Blobs, reparse_limit: Int, name: Document.Node.Name, perspective: Command.Perspective, @@ -369,7 +369,7 @@ last = it.next i += last.length } - reparse_spans(thy_load, syntax, all_blobs, name, commands, first_unfinished, last) + reparse_spans(thy_load, syntax, doc_blobs, name, commands, first_unfinished, last) case None => commands } case None => commands @@ -393,7 +393,7 @@ private def text_edit( thy_load: Thy_Load, syntax: Outer_Syntax, - all_blobs: Map[Document.Node.Name, Bytes], + doc_blobs: Document.Blobs, reparse_limit: Int, node: Document.Node, edit: Document.Edit_Text): Document.Node = { @@ -404,7 +404,7 @@ val commands0 = node.commands val commands1 = edit_text(text_edits, commands0) val commands2 = - recover_spans(thy_load, syntax, all_blobs, name, node.perspective.visible, commands1) + recover_spans(thy_load, syntax, doc_blobs, name, node.perspective.visible, commands1) node.update_commands(commands2) case (_, Document.Node.Deps(_)) => node @@ -416,10 +416,10 @@ if (node.same_perspective(perspective)) node else node.update_perspective(perspective).update_commands( - consolidate_spans(thy_load, syntax, all_blobs, reparse_limit, + consolidate_spans(thy_load, syntax, doc_blobs, reparse_limit, name, visible, node.commands)) - case (_, Document.Node.Blob(_)) => node + case (_, Document.Node.Blob()) => node } } @@ -427,56 +427,53 @@ thy_load: Thy_Load, reparse_limit: Int, previous: Document.Version, + doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) - : (Map[Document.Node.Name, Bytes], List[Document.Edit_Command], Document.Version) = + : (List[Document.Edit_Command], Document.Version) = { val (syntax, reparse0, nodes0, doc_edits0) = header_edits(thy_load.base_syntax, previous, edits) - val reparse = - (reparse0 /: nodes0.entries)({ - case (reparse, (name, node)) => - if (node.thy_load_commands.isEmpty) reparse - else name :: reparse - }) - val reparse_set = reparse.toSet + if (edits.isEmpty) + (Nil, Document.Version.make(syntax, previous.nodes)) + else { + val reparse = + (reparse0 /: nodes0.entries)({ + case (reparse, (name, node)) => + if (node.thy_load_commands.isEmpty) reparse + else name :: reparse + }) + val reparse_set = reparse.toSet - var nodes = nodes0 - val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0 + var nodes = nodes0 + val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0 + + val node_edits = + (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1) + .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]] // FIXME ??? - val node_edits = - (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1) - .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]] // FIXME ??? + node_edits foreach { + case (name, edits) => + val node = nodes(name) + val commands = node.commands - val all_blobs: Map[Document.Node.Name, Bytes] = - (Map.empty[Document.Node.Name, Bytes] /: node_edits) { - case (bs1, (_, es)) => (bs1 /: es) { - case (bs, (name, Document.Node.Blob(blob))) => bs + (name -> blob) - case (bs, _) => bs - } + val node1 = + if (reparse_set(name) && !commands.isEmpty) + node.update_commands( + reparse_spans(thy_load, syntax, doc_blobs, + name, commands, commands.head, commands.last)) + else node + val node2 = (node1 /: edits)(text_edit(thy_load, syntax, doc_blobs, reparse_limit, _, _)) + + if (!(node.same_perspective(node2.perspective))) + doc_edits += (name -> node2.perspective) + + doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands))) + + nodes += (name -> node2) } - node_edits foreach { - case (name, edits) => - val node = nodes(name) - val commands = node.commands - - val node1 = - if (reparse_set(name) && !commands.isEmpty) - node.update_commands( - reparse_spans(thy_load, syntax, all_blobs, - name, commands, commands.head, commands.last)) - else node - val node2 = (node1 /: edits)(text_edit(thy_load, syntax, all_blobs, reparse_limit, _, _)) - - if (!(node.same_perspective(node2.perspective))) - doc_edits += (name -> node2.perspective) - - doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands))) - - nodes += (name -> node2) + (doc_edits.toList, Document.Version.make(syntax, nodes)) } - - (all_blobs, doc_edits.toList, Document.Version.make(syntax, nodes)) } } diff -r cee77d2e9582 -r 744ea0025e11 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Tue Nov 19 19:43:26 2013 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Tue Nov 19 20:53:43 2013 +0100 @@ -148,7 +148,7 @@ node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))), node_name -> perspective) else - List(node_name -> Document.Node.Blob(blob())) + List(node_name -> Document.Node.Blob()) } def node_edits( @@ -171,7 +171,7 @@ node_name -> perspective) } else - List(node_name -> Document.Node.Blob(blob())) + List(node_name -> Document.Node.Blob()) } @@ -190,7 +190,7 @@ val clear = pending_clear val edits = snapshot() val perspective = node_perspective() - if (!is_theory || clear || !edits.isEmpty || last_perspective != perspective) { + if (clear || !edits.isEmpty || last_perspective != perspective) { pending_clear = false pending.clear last_perspective = perspective diff -r cee77d2e9582 -r 744ea0025e11 src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Tue Nov 19 19:43:26 2013 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Nov 19 20:53:43 2013 +0100 @@ -19,21 +19,21 @@ override def session: Session = PIDE.session + def document_models(): List[Document_Model] = + for { + buffer <- JEdit_Lib.jedit_buffers().toList + model <- PIDE.document_model(buffer) + } yield model + + def document_blobs(): Document.Blobs = + document_models().filterNot(_.is_theory).map(model => (model.node_name -> model.blob())).toMap + override def flush() { Swing_Thread.require() - session.update( - (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) { - case (edits, buffer) => - JEdit_Lib.buffer_lock(buffer) { - PIDE.document_model(buffer) match { - case Some(model) => model.flushed_edits() ::: edits - case None => edits - } - } - } - ) + val edits = document_models().flatMap(_.flushed_edits()) + if (!edits.isEmpty) session.update(document_blobs(), edits) } private val delay_flush = diff -r cee77d2e9582 -r 744ea0025e11 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Tue Nov 19 19:43:26 2013 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Tue Nov 19 20:53:43 2013 +0100 @@ -113,7 +113,7 @@ model_edits ::: edits } } - session.update(init_edits) + session.update(PIDE.editor.document_blobs(), init_edits) } }