tuned signature -- emphasize special nature of protocol commands;

--- a/src/Pure/PIDE/protocol.ML	Thu Jan 05 10:59:18 2012 +0100
+++ b/src/Pure/PIDE/protocol.ML	Thu Jan 05 13:24:29 2012 +0100
@@ -8,16 +8,16 @@
 struct
 
 val _ =
-  Isabelle_Process.add_command "Document.define_command"
+  Isabelle_Process.protocol_command "Document.define_command"
     (fn [id, name, text] =>
       Document.change_state (Document.define_command (Document.parse_id id) name text));
 
 val _ =
-  Isabelle_Process.add_command "Document.cancel_execution"
+  Isabelle_Process.protocol_command "Document.cancel_execution"
     (fn [] => ignore (Document.cancel_execution (Document.state ())));
 
 val _ =
-  Isabelle_Process.add_command "Document.update_perspective"
+  Isabelle_Process.protocol_command "Document.update_perspective"
     (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
       let
         val old_id = Document.parse_id old_id_string;
@@ -33,7 +33,7 @@
       end));
 
 val _ =
-  Isabelle_Process.add_command "Document.update"
+  Isabelle_Process.protocol_command "Document.update"
     (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
       let
         val old_id = Document.parse_id old_id_string;
@@ -66,7 +66,7 @@
       in state2 end));
 
 val _ =
-  Isabelle_Process.add_command "Document.remove_versions"
+  Isabelle_Process.protocol_command "Document.remove_versions"
     (fn [versions_yxml] => Document.change_state (fn state =>
       let
         val versions =
@@ -77,7 +77,7 @@
       in state1 end));
 
 val _ =
-  Isabelle_Process.add_command "Document.invoke_scala"
+  Isabelle_Process.protocol_command "Document.invoke_scala"
     (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res);
 
 end;

--- a/src/Pure/System/isabelle_process.ML	Thu Jan 05 10:59:18 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML	Thu Jan 05 13:24:29 2012 +0100
@@ -18,8 +18,7 @@
 signature ISABELLE_PROCESS =
 sig
   val is_active: unit -> bool
-  val add_command: string -> (string list -> unit) -> unit
-  val command: string -> string list -> unit
+  val protocol_command: string -> (string list -> unit) -> unit
   val crashes: exn list Synchronized.var
   val init_fifos: string -> string -> unit
   val init_socket: string -> unit
@@ -38,7 +37,7 @@
 val _ = Markup.add_mode isabelle_processN YXML.output_markup;
 
 
-(* commands *)
+(* protocol commands *)
 
 local
 
@@ -47,16 +46,18 @@
 
 in
 
-fun add_command name cmd =
+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);
     Symtab.update (name, cmd) cmds));
 
-fun command name args =
+fun run_command name args =
   (case Symtab.lookup (Synchronized.value commands) name of
     NONE => error ("Undefined Isabelle process command " ^ quote name)
-  | SOME cmd => cmd args);
+  | SOME cmd =>
+      (Runtime.debugging cmd args handle exn =>
+        error ("Isabelle process protocol failure: " ^ name ^ "\n" ^ ML_Compiler.exn_message exn)));
 
 end;
 
@@ -145,11 +146,6 @@
     NONE => raise Runtime.TERMINATE
   | SOME line => map (read_chunk channel) (space_explode "," line));
 
-fun run_command name args =
-  Runtime.debugging (command name) args
-    handle exn =>
-      error ("Isabelle process command failure: " ^ name ^ "\n" ^ ML_Compiler.exn_message exn);
-
 in
 
 fun loop channel =