# HG changeset patch
# User wenzelm
# Date 1567791894 -7200
# Node ID 94442fce40a556d1e33c78b6b3fcea0ceafc2322
# Parent  2bd9e30183b1437485d775a2eb63cc398b476559
prefer commands_accepted: fewer protocol messages;

diff -r 2bd9e30183b1 -r 94442fce40a5 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Sep 06 18:59:24 2019 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Sep 06 19:44:54 2019 +0200
@@ -438,9 +438,6 @@
       val commands' =
         Inttab.update_new (command_id, (name, blobs_digests, blobs_index, span)) commands
           handle Inttab.DUP dup => err_dup "command" dup;
-      val _ =
-        Position.setmp_thread_data (Position.id_only id)
-          (fn () => Output.status [Markup.markup_only Markup.accepted]) ();
     in (versions, blobs, commands', execution) end);
 
 fun the_command (State {commands, ...}) command_id =
diff -r 2bd9e30183b1 -r 94442fce40a5 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Sep 06 18:59:24 2019 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Sep 06 19:44:54 2019 +0200
@@ -174,7 +174,6 @@
   val goalN: string val goal: T
   val subgoalN: string val subgoal: string -> T
   val taskN: string
-  val acceptedN: string val accepted: T
   val forkedN: string val forked: T
   val joinedN: string val joined: T
   val runningN: string val running: T
@@ -211,6 +210,7 @@
   val dialogN: string val dialog: serial -> string -> T
   val jedit_actionN: string
   val functionN: string
+  val commands_accepted: Properties.T
   val assign_update: Properties.T
   val removed_versions: Properties.T
   val protocol_handler: string -> Properties.T
@@ -623,7 +623,6 @@
 
 val taskN = "task";
 
-val (acceptedN, accepted) = markup_elem "accepted";
 val (forkedN, forked) = markup_elem "forked";
 val (joinedN, joined) = markup_elem "joined";
 val (runningN, running) = markup_elem "running";
@@ -682,6 +681,8 @@
 
 val functionN = "function"
 
+val commands_accepted = [(functionN, "commands_accepted")];
+
 val assign_update = [(functionN, "assign_update")];
 val removed_versions = [(functionN, "removed_versions")];
 
diff -r 2bd9e30183b1 -r 94442fce40a5 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Sep 06 18:59:24 2019 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Sep 06 19:44:54 2019 +0200
@@ -553,6 +553,7 @@
   val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing")
   val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing")
 
+  val Commands_Accepted: Properties.T = List((FUNCTION, "commands_accepted"))
   val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
   val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
 
diff -r 2bd9e30183b1 -r 94442fce40a5 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Fri Sep 06 18:59:24 2019 +0200
+++ b/src/Pure/PIDE/protocol.ML	Fri Sep 06 19:44:54 2019 +0200
@@ -62,12 +62,15 @@
     tokens = toks ~~ sources}
   end;
 
+fun commands_accepted ids = Output.protocol_message Markup.commands_accepted [commas ids];
+
 val _ =
   Isabelle_Process.protocol_command "Document.define_command"
     (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 _ = Document.change_state (Document.define_command command);
+      in commands_accepted [id] end);
 
 val _ =
   Isabelle_Process.protocol_command "Document.define_commands"
@@ -79,7 +82,10 @@
             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 commands = map decode args;
+        val _ = Document.change_state (fold Document.define_command commands);
+      in commands_accepted (map (Value.print_int o #command_id) commands) end);
 
 val _ =
   Isabelle_Process.protocol_command "Document.discontinue_execution"
diff -r 2bd9e30183b1 -r 94442fce40a5 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Sep 06 18:59:24 2019 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Sep 06 19:44:54 2019 +0200
@@ -11,6 +11,15 @@
 {
   /* document editing */
 
+  object Commands_Accepted
+  {
+    def unapply(text: String): Option[List[Document_ID.Command]] =
+      try { Some(space_explode(',', text).map(Value.Long.parse)) }
+      catch { case ERROR(_) => None }
+
+    val message: XML.Elem = XML.elem(Markup.STATUS, List(XML.elem(Markup.ACCEPTED)))
+  }
+
   object Assign_Update
   {
     def unapply(text: String)
diff -r 2bd9e30183b1 -r 94442fce40a5 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Sep 06 18:59:24 2019 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Sep 06 19:44:54 2019 +0200
@@ -503,6 +503,14 @@
                 val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
                 change_command(_.add_export(id, (args.serial, export)))
 
+              case Markup.Commands_Accepted =>
+                msg.text match {
+                  case Protocol.Commands_Accepted(ids) =>
+                    ids.foreach(id =>
+                      change_command(_.accumulate(id, Protocol.Commands_Accepted.message, xml_cache)))
+                  case _ => bad_output()
+                }
+
               case Markup.Assign_Update =>
                 msg.text match {
                   case Protocol.Assign_Update(id, edited, update) =>