src/Pure/PIDE/protocol.ML

--- a/src/Pure/PIDE/protocol.ML	Fri Dec 18 12:57:25 2020 +0100
+++ b/src/Pure/PIDE/protocol.ML	Fri Dec 18 23:19:07 2020 +0100
@@ -31,9 +31,10 @@
   Isabelle_Process.protocol_command "Document.define_blob"
     (fn [digest, content] => Document.change_state (Document.define_blob digest content));
 
-fun decode_command id name blobs_xml toks_xml sources : Document.command =
+fun decode_command id name parents_xml blobs_xml toks_xml sources : Document.command =
   let
     open XML.Decode;
+    val parents = list string parents_xml;
     val (blobs_digests, blobs_index) =
       blobs_xml |>
         let
@@ -52,6 +53,7 @@
   in
    {command_id = Document_ID.parse id,
     name = name,
+    parents = parents,
     blobs_digests = blobs_digests,
     blobs_index = blobs_index,
     tokens = toks ~~ sources}
@@ -62,9 +64,11 @@
 
 val _ =
   Isabelle_Process.protocol_command "Document.define_command"
-    (fn id :: name :: blobs :: toks :: sources =>
+    (fn id :: name :: parents :: blobs :: toks :: sources =>
       let
-        val command = decode_command id name (YXML.parse_body blobs) (YXML.parse_body toks) sources;
+        val command =
+          decode_command id name (YXML.parse_body parents) (YXML.parse_body blobs)
+            (YXML.parse_body toks) sources;
         val _ = Document.change_state (Document.define_command command);
       in commands_accepted [id] end);
 
@@ -75,9 +79,10 @@
         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;
+            val (id, (name, (parents_xml, (blobs_xml, (toks_xml, sources))))) =
+              pair string (pair string (pair I (pair I (pair I (list string)))))
+                (YXML.parse_body arg);
+          in decode_command id name parents_xml blobs_xml toks_xml sources end;
 
         val commands = map decode args;
         val _ = Document.change_state (fold Document.define_command commands);