src/Pure/PIDE/protocol.scala
changeset 54519 5fed81762406
parent 54515 570ba266f5b5
child 54524 14609d36cab8
equal deleted inserted replaced
54518:81a9a54c57fc 54519:5fed81762406
   306 }
   306 }
   307 
   307 
   308 
   308 
   309 trait Protocol extends Isabelle_Process
   309 trait Protocol extends Isabelle_Process
   310 {
   310 {
       
   311   /* inlined files */
       
   312 
       
   313   def define_blob(blob: Bytes): Unit =
       
   314     protocol_command_raw("Document.define_blob", Bytes(blob.sha1_digest.toString), blob)
       
   315 
       
   316 
   311   /* commands */
   317   /* commands */
   312 
   318 
   313   def define_command(command: Command): Unit =
   319   def define_command(command: Command): Unit =
       
   320   {
       
   321     val blobs_yxml =
       
   322     { import XML.Encode._
       
   323       val encode_blob: T[Command.Blob] =
       
   324         variant(List(
       
   325           { case Exn.Res((a, b)) => (List(a.node, b.toString), Nil) },
       
   326           { case Exn.Exn(e) => (List(Exn.message(e)), Nil) }))
       
   327       YXML.string_of_body(list(encode_blob)(command.blobs))
       
   328     }
   314     protocol_command("Document.define_command",
   329     protocol_command("Document.define_command",
   315       Document_ID(command.id), encode(command.name), encode(command.source))
   330       Document_ID(command.id), encode(command.name), blobs_yxml, encode(command.source))
       
   331   }
   316 
   332 
   317 
   333 
   318   /* execution */
   334   /* execution */
   319 
   335 
   320   def discontinue_execution(): Unit =
   336   def discontinue_execution(): Unit =