equal
deleted
inserted
replaced
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 = |