src/Pure/System/isabelle_process.ML
changeset 46119 0d7172a7672c
parent 45666 d83797ef0d2d
child 46121 30a69cd8a9a0
     1.1 --- a/src/Pure/System/isabelle_process.ML	Thu Jan 05 10:59:18 2012 +0100
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Thu Jan 05 13:24:29 2012 +0100
     1.3 @@ -18,8 +18,7 @@
     1.4  signature ISABELLE_PROCESS =
     1.5  sig
     1.6    val is_active: unit -> bool
     1.7 -  val add_command: string -> (string list -> unit) -> unit
     1.8 -  val command: string -> string list -> unit
     1.9 +  val protocol_command: string -> (string list -> unit) -> unit
    1.10    val crashes: exn list Synchronized.var
    1.11    val init_fifos: string -> string -> unit
    1.12    val init_socket: string -> unit
    1.13 @@ -38,7 +37,7 @@
    1.14  val _ = Markup.add_mode isabelle_processN YXML.output_markup;
    1.15  
    1.16  
    1.17 -(* commands *)
    1.18 +(* protocol commands *)
    1.19  
    1.20  local
    1.21  
    1.22 @@ -47,16 +46,18 @@
    1.23  
    1.24  in
    1.25  
    1.26 -fun add_command name cmd =
    1.27 +fun protocol_command name cmd =
    1.28    Synchronized.change commands (fn cmds =>
    1.29     (if not (Symtab.defined cmds name) then ()
    1.30      else warning ("Redefining Isabelle process command " ^ quote name);
    1.31      Symtab.update (name, cmd) cmds));
    1.32  
    1.33 -fun command name args =
    1.34 +fun run_command name args =
    1.35    (case Symtab.lookup (Synchronized.value commands) name of
    1.36      NONE => error ("Undefined Isabelle process command " ^ quote name)
    1.37 -  | SOME cmd => cmd args);
    1.38 +  | SOME cmd =>
    1.39 +      (Runtime.debugging cmd args handle exn =>
    1.40 +        error ("Isabelle process protocol failure: " ^ name ^ "\n" ^ ML_Compiler.exn_message exn)));
    1.41  
    1.42  end;
    1.43  
    1.44 @@ -145,11 +146,6 @@
    1.45      NONE => raise Runtime.TERMINATE
    1.46    | SOME line => map (read_chunk channel) (space_explode "," line));
    1.47  
    1.48 -fun run_command name args =
    1.49 -  Runtime.debugging (command name) args
    1.50 -    handle exn =>
    1.51 -      error ("Isabelle process command failure: " ^ name ^ "\n" ^ ML_Compiler.exn_message exn);
    1.52 -
    1.53  in
    1.54  
    1.55  fun loop channel =