src/Pure/PIDE/protocol.scala
changeset 52582 31467a4b1466
parent 52563 f9a20c2c3b70
child 52650 4cf6fbf1d9a1
--- a/src/Pure/PIDE/protocol.scala	Wed Jul 10 21:54:43 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala	Wed Jul 10 22:04:57 2013 +0200
@@ -308,15 +308,15 @@
   /* commands */
 
   def define_command(command: Command): Unit =
-    input("Document.define_command",
+    protocol_command("Document.define_command",
       Document_ID(command.id), encode(command.name), encode(command.source))
 
 
   /* document versions */
 
-  def discontinue_execution() { input("Document.discontinue_execution") }
+  def discontinue_execution() { protocol_command("Document.discontinue_execution") }
 
-  def cancel_execution() { input("Document.cancel_execution") }
+  def cancel_execution() { protocol_command("Document.cancel_execution") }
 
   def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
     edits: List[Document.Edit_Command])
@@ -346,7 +346,7 @@
         pair(string, encode_edit(name))(name.node, edit)
       })
       YXML.string_of_body(encode_edits(edits)) }
-    input("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml)
+    protocol_command("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml)
   }
 
   def remove_versions(versions: List[Document.Version])
@@ -354,7 +354,7 @@
     val versions_yxml =
       { import XML.Encode._
         YXML.string_of_body(list(long)(versions.map(_.id))) }
-    input("Document.remove_versions", versions_yxml)
+    protocol_command("Document.remove_versions", versions_yxml)
   }
 
 
@@ -362,6 +362,6 @@
 
   def dialog_result(serial: Long, result: String)
   {
-    input("Document.dialog_result", Properties.Value.Long(serial), result)
+    protocol_command("Document.dialog_result", Properties.Value.Long(serial), result)
   }
 }