src/Pure/PIDE/protocol.scala
changeset 52931 ac6648c0c0fb
parent 52862 930ce8eacb87
child 54509 1f77110c94ef
     1.1 --- a/src/Pure/PIDE/protocol.scala	Fri Aug 09 10:41:17 2013 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Aug 09 11:18:36 2013 +0200
     1.3 @@ -315,9 +315,16 @@
     1.4        Document_ID(command.id), encode(command.name), encode(command.source))
     1.5  
     1.6  
     1.7 -  /* document versions */
     1.8 +  /* execution */
     1.9 +
    1.10 +  def discontinue_execution(): Unit =
    1.11 +    protocol_command("Document.discontinue_execution")
    1.12  
    1.13 -  def discontinue_execution() { protocol_command("Document.discontinue_execution") }
    1.14 +  def cancel_exec(id: Document_ID.Exec): Unit =
    1.15 +    protocol_command("Document.cancel_exec", Document_ID(id))
    1.16 +
    1.17 +
    1.18 +  /* document versions */
    1.19  
    1.20    def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
    1.21      edits: List[Document.Edit_Command])
    1.22 @@ -363,8 +370,6 @@
    1.23  
    1.24    /* dialog via document content */
    1.25  
    1.26 -  def dialog_result(serial: Long, result: String)
    1.27 -  {
    1.28 +  def dialog_result(serial: Long, result: String): Unit =
    1.29      protocol_command("Document.dialog_result", Properties.Value.Long(serial), result)
    1.30 -  }
    1.31  }