prefer define_commands_bulk: fewer protocol messages;
authorwenzelm
Fri, 06 Sep 2019 18:59:24 +0200
changeset 70854 2bd9e30183b1
parent 70853 4a358f8c7cb7
child 70855 94442fce40a5
prefer define_commands_bulk: fewer protocol messages;
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/session.scala
--- 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"
--- 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)
+    }
   }
 
 
--- 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