tuned signature;

--- 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)
   }
 }

--- a/src/Pure/System/invoke_scala.scala	Wed Jul 10 21:54:43 2013 +0200
+++ b/src/Pure/System/invoke_scala.scala	Wed Jul 10 22:04:57 2013 +0200
@@ -76,7 +76,7 @@
     id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit = synchronized
   {
     if (futures.isDefinedAt(id)) {
-      prover.input("Invoke_Scala.fulfill", id, tag.toString, res)
+      prover.protocol_command("Invoke_Scala.fulfill", id, tag.toString, res)
       futures -= id
     }
   }

--- a/src/Pure/System/isabelle_process.ML	Wed Jul 10 21:54:43 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed Jul 10 22:04:57 2013 +0200
@@ -48,15 +48,15 @@
 fun protocol_command name cmd =
   Synchronized.change commands (fn cmds =>
    (if not (Symtab.defined cmds name) then ()
-    else warning ("Redefining Isabelle process command " ^ quote name);
+    else warning ("Redefining Isabelle protocol command " ^ quote name);
     Symtab.update (name, cmd) cmds));
 
 fun run_command name args =
   (case Symtab.lookup (Synchronized.value commands) name of
-    NONE => error ("Undefined Isabelle process command " ^ quote name)
+    NONE => error ("Undefined Isabelle protocol command " ^ quote name)
   | SOME cmd =>
       (Runtime.debugging cmd args handle exn =>
-        error ("Isabelle process protocol failure: " ^ quote name ^ "\n" ^
+        error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^
           ML_Compiler.exn_message exn)));
 
 end;

--- a/src/Pure/System/isabelle_process.scala	Wed Jul 10 21:54:43 2013 +0200
+++ b/src/Pure/System/isabelle_process.scala	Wed Jul 10 22:04:57 2013 +0200
@@ -354,15 +354,15 @@
 
   /** main methods **/
 
-  def input_bytes(name: String, args: Array[Byte]*): Unit =
+  def protocol_command_raw(name: String, args: Array[Byte]*): Unit =
     command_input._2 ! Input_Chunks(UTF8.string_bytes(name) :: args.toList)
 
-  def input(name: String, args: String*)
+  def protocol_command(name: String, args: String*)
   {
     receiver(new Input(name, args.toList))
-    input_bytes(name, args.map(UTF8.string_bytes): _*)
+    protocol_command_raw(name, args.map(UTF8.string_bytes): _*)
   }
 
   def options(opts: Options): Unit =
-    input("Isabelle_Process.options", YXML.string_of_body(opts.encode))
+    protocol_command("Isabelle_Process.options", YXML.string_of_body(opts.encode))
 }