src/Pure/PIDE/protocol.ML

--- a/src/Pure/PIDE/protocol.ML	Tue Nov 19 13:54:02 2013 +0100
+++ b/src/Pure/PIDE/protocol.ML	Tue Nov 19 19:33:27 2013 +0100
@@ -23,9 +23,23 @@
       end);
 
 val _ =
+  Isabelle_Process.protocol_command "Document.define_blob"
+    (fn [digest, content] => Document.change_state (Document.define_blob digest content));
+
+val _ =
   Isabelle_Process.protocol_command "Document.define_command"
-    (fn [id, name, text] =>
-      Document.change_state (Document.define_command (Document_ID.parse id) name text));
+    (fn [id, name, blobs_yxml, text] =>
+      let
+        val blobs =
+          YXML.parse_body blobs_yxml |>
+            let open XML.Decode in
+              list (variant
+               [fn ([a, b], []) => Exn.Res (a, b),
+                fn ([a], []) => Exn.Exn (ERROR a)])
+            end;
+      in
+        Document.change_state (Document.define_command (Document_ID.parse id) name blobs text)
+      end);
 
 val _ =
   Isabelle_Process.protocol_command "Document.discontinue_execution"