src/Pure/PIDE/protocol.scala
changeset 52931 ac6648c0c0fb
parent 52862 930ce8eacb87
child 54509 1f77110c94ef
--- a/src/Pure/PIDE/protocol.scala	Fri Aug 09 10:41:17 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Aug 09 11:18:36 2013 +0200
@@ -315,9 +315,16 @@
       Document_ID(command.id), encode(command.name), encode(command.source))
 
 
-  /* document versions */
+  /* execution */
+
+  def discontinue_execution(): Unit =
+    protocol_command("Document.discontinue_execution")
 
-  def discontinue_execution() { protocol_command("Document.discontinue_execution") }
+  def cancel_exec(id: Document_ID.Exec): Unit =
+    protocol_command("Document.cancel_exec", Document_ID(id))
+
+
+  /* document versions */
 
   def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
     edits: List[Document.Edit_Command])
@@ -363,8 +370,6 @@
 
   /* dialog via document content */
 
-  def dialog_result(serial: Long, result: String)
-  {
+  def dialog_result(serial: Long, result: String): Unit =
     protocol_command("Document.dialog_result", Properties.Value.Long(serial), result)
-  }
 }