# HG changeset patch # User wenzelm # Date 1567789164 -7200 # Node ID 2bd9e30183b1437485d775a2eb63cc398b476559 # Parent 4a358f8c7cb735e876e0eee508f56c4d8d53f875 prefer define_commands_bulk: fewer protocol messages; diff -r 4a358f8c7cb7 -r 2bd9e30183b1 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Fri Sep 06 17:10:23 2019 +0200 +++ b/src/Pure/PIDE/protocol.ML Fri Sep 06 18:59:24 2019 +0200 @@ -39,11 +39,11 @@ Isabelle_Process.protocol_command "Document.define_blob" (fn [digest, content] => Document.change_state (Document.define_blob digest content)); -fun decode_command id name blobs_yxml toks_yxml sources : Document.command = +fun decode_command id name blobs_xml toks_xml sources : Document.command = let open XML.Decode; val (blobs_digests, blobs_index) = - YXML.parse_body blobs_yxml |> + blobs_xml |> let val message = YXML.string_of_body o Protocol_Message.command_positions id; in @@ -53,7 +53,7 @@ fn ([], a) => Exn.Exn (ERROR (message a))])) int end; - val toks = YXML.parse_body toks_yxml |> list (pair int int); + val toks = list (pair int int) toks_xml; in {command_id = Document_ID.parse id, name = name, @@ -64,9 +64,22 @@ val _ = Isabelle_Process.protocol_command "Document.define_command" - (fn id :: name :: blobs_yxml :: toks_yxml :: sources => - Document.change_state - (Document.define_command (decode_command id name blobs_yxml toks_yxml sources))); + (fn id :: name :: blobs :: toks :: sources => + let + val command = decode_command id name (YXML.parse_body blobs) (YXML.parse_body toks) sources; + in Document.change_state (Document.define_command command) end); + +val _ = + Isabelle_Process.protocol_command "Document.define_commands" + (fn args => + let + fun decode arg = + let + open XML.Decode; + val (id, (name, (blobs_xml, (toks_xml, sources)))) = + pair string (pair string (pair I (pair I (list string)))) (YXML.parse_body arg); + in decode_command id name blobs_xml toks_xml sources end; + in Document.change_state (fold (Document.define_command o decode) args) end); val _ = Isabelle_Process.protocol_command "Document.discontinue_execution" diff -r 4a358f8c7cb7 -r 2bd9e30183b1 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Fri Sep 06 17:10:23 2019 +0200 +++ b/src/Pure/PIDE/protocol.scala Fri Sep 06 18:59:24 2019 +0200 @@ -245,11 +245,12 @@ def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit = protocol_command_raw("Document.define_blob", List(Bytes(digest.toString), bytes)) - def define_command(command: Command) + private def encode_command(command: Command): (String, String, String, String, List[String]) = { + import XML.Encode._ + val blobs_yxml = { - import XML.Encode._ val encode_blob: T[Command.Blob] = variant(List( { case Exn.Res((a, b)) => @@ -259,17 +260,46 @@ Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index)) } - val toks = command.span.content val toks_yxml = { - import XML.Encode._ val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source)))) - Symbol.encode_yxml(list(encode_tok)(toks)) + Symbol.encode_yxml(list(encode_tok)(command.span.content)) } + val toks_sources = command.span.content.map(tok => Symbol.encode(tok.source)) - protocol_command_args("Document.define_command", - Document_ID(command.id) :: Symbol.encode(command.span.name) :: blobs_yxml :: toks_yxml :: - toks.map(tok => Symbol.encode(tok.source))) + (Document_ID(command.id), Symbol.encode(command.span.name), blobs_yxml, toks_yxml, toks_sources) + } + + def define_command(command: Command) + { + val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command) + protocol_command_args( + "Document.define_command", command_id :: name :: blobs_yxml :: toks_yxml :: toks_sources) + } + + def define_commands(commands: List[Command]) + { + protocol_command_args("Document.define_commands", + commands.map(command => + { + import XML.Encode._ + val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command) + val body = + pair(string, pair(string, pair(string, pair(string, list(string)))))( + command_id, (name, (blobs_yxml, (toks_yxml, toks_sources)))) + YXML.string_of_body(body) + })) + } + + def define_commands_bulk(commands: List[Command]) + { + val (irregular, regular) = commands.partition(command => YXML.detect(command.source)) + irregular.foreach(define_command(_)) + regular match { + case Nil => + case List(command) => define_command(command) + case _ => define_commands(regular) + } } diff -r 4a358f8c7cb7 -r 2bd9e30183b1 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Fri Sep 06 17:10:23 2019 +0200 +++ b/src/Pure/PIDE/session.scala Fri Sep 06 18:59:24 2019 +0200 @@ -9,6 +9,7 @@ import scala.collection.immutable.Queue +import scala.collection.mutable import scala.annotation.tailrec @@ -420,28 +421,33 @@ { require(prover.defined) - def id_command(command: Command) + // define commands { - for { - (name, digest) <- command.blobs_defined - if !global_state.value.defined_blob(digest) - } { - change.version.nodes(name).get_blob match { - case Some(blob) => - global_state.change(_.define_blob(digest)) - prover.get.define_blob(digest, blob.bytes) - case None => - Output.error_message("Missing blob " + quote(name.toString)) + val id_commands = new mutable.ListBuffer[Command] + def id_command(command: Command) + { + for { + (name, digest) <- command.blobs_defined + if !global_state.value.defined_blob(digest) + } { + change.version.nodes(name).get_blob match { + case Some(blob) => + global_state.change(_.define_blob(digest)) + prover.get.define_blob(digest, blob.bytes) + case None => + Output.error_message("Missing blob " + quote(name.toString)) + } + } + + if (!global_state.value.defined_command(command.id)) { + global_state.change(_.define_command(command)) + id_commands += command } } - - if (!global_state.value.defined_command(command.id)) { - global_state.change(_.define_command(command)) - prover.get.define_command(command) + for { (_, edit) <- change.doc_edits } { + edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) }) } - } - for { (_, edit) <- change.doc_edits } { - edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) }) + if (id_commands.nonEmpty) prover.get.define_commands_bulk(id_commands.toList) } val assignment = global_state.value.the_assignment(change.previous).check_finished