--- 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