src/Pure/System/isabelle_process.ML

--- 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 =