src/Pure/PIDE/protocol.scala
changeset 54519 5fed81762406
parent 54515 570ba266f5b5
child 54524 14609d36cab8
--- a/src/Pure/PIDE/protocol.scala	Tue Nov 19 13:54:02 2013 +0100
+++ b/src/Pure/PIDE/protocol.scala	Tue Nov 19 19:33:27 2013 +0100
@@ -308,11 +308,27 @@
 
 trait Protocol extends Isabelle_Process
 {
+  /* inlined files */
+
+  def define_blob(blob: Bytes): Unit =
+    protocol_command_raw("Document.define_blob", Bytes(blob.sha1_digest.toString), blob)
+
+
   /* commands */
 
   def define_command(command: Command): Unit =
+  {
+    val blobs_yxml =
+    { import XML.Encode._
+      val encode_blob: T[Command.Blob] =
+        variant(List(
+          { case Exn.Res((a, b)) => (List(a.node, b.toString), Nil) },
+          { case Exn.Exn(e) => (List(Exn.message(e)), Nil) }))
+      YXML.string_of_body(list(encode_blob)(command.blobs))
+    }
     protocol_command("Document.define_command",
-      Document_ID(command.id), encode(command.name), encode(command.source))
+      Document_ID(command.id), encode(command.name), blobs_yxml, encode(command.source))
+  }
 
 
   /* execution */