tuned signature -- emphasize special nature of protocol commands;
authorwenzelm
Thu Jan 05 13:24:29 2012 +0100 (2012-01-05)
changeset 461190d7172a7672c
parent 46118 e99ca055c91d
child 46120 f7ee2e5a83dd
tuned signature -- emphasize special nature of protocol commands;
src/Pure/PIDE/protocol.ML
src/Pure/System/isabelle_process.ML
     1.1 --- a/src/Pure/PIDE/protocol.ML	Thu Jan 05 10:59:18 2012 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Jan 05 13:24:29 2012 +0100
     1.3 @@ -8,16 +8,16 @@
     1.4  struct
     1.5  
     1.6  val _ =
     1.7 -  Isabelle_Process.add_command "Document.define_command"
     1.8 +  Isabelle_Process.protocol_command "Document.define_command"
     1.9      (fn [id, name, text] =>
    1.10        Document.change_state (Document.define_command (Document.parse_id id) name text));
    1.11  
    1.12  val _ =
    1.13 -  Isabelle_Process.add_command "Document.cancel_execution"
    1.14 +  Isabelle_Process.protocol_command "Document.cancel_execution"
    1.15      (fn [] => ignore (Document.cancel_execution (Document.state ())));
    1.16  
    1.17  val _ =
    1.18 -  Isabelle_Process.add_command "Document.update_perspective"
    1.19 +  Isabelle_Process.protocol_command "Document.update_perspective"
    1.20      (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
    1.21        let
    1.22          val old_id = Document.parse_id old_id_string;
    1.23 @@ -33,7 +33,7 @@
    1.24        end));
    1.25  
    1.26  val _ =
    1.27 -  Isabelle_Process.add_command "Document.update"
    1.28 +  Isabelle_Process.protocol_command "Document.update"
    1.29      (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
    1.30        let
    1.31          val old_id = Document.parse_id old_id_string;
    1.32 @@ -66,7 +66,7 @@
    1.33        in state2 end));
    1.34  
    1.35  val _ =
    1.36 -  Isabelle_Process.add_command "Document.remove_versions"
    1.37 +  Isabelle_Process.protocol_command "Document.remove_versions"
    1.38      (fn [versions_yxml] => Document.change_state (fn state =>
    1.39        let
    1.40          val versions =
    1.41 @@ -77,7 +77,7 @@
    1.42        in state1 end));
    1.43  
    1.44  val _ =
    1.45 -  Isabelle_Process.add_command "Document.invoke_scala"
    1.46 +  Isabelle_Process.protocol_command "Document.invoke_scala"
    1.47      (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res);
    1.48  
    1.49  end;
     2.1 --- a/src/Pure/System/isabelle_process.ML	Thu Jan 05 10:59:18 2012 +0100
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Thu Jan 05 13:24:29 2012 +0100
     2.3 @@ -18,8 +18,7 @@
     2.4  signature ISABELLE_PROCESS =
     2.5  sig
     2.6    val is_active: unit -> bool
     2.7 -  val add_command: string -> (string list -> unit) -> unit
     2.8 -  val command: string -> string list -> unit
     2.9 +  val protocol_command: string -> (string list -> unit) -> unit
    2.10    val crashes: exn list Synchronized.var
    2.11    val init_fifos: string -> string -> unit
    2.12    val init_socket: string -> unit
    2.13 @@ -38,7 +37,7 @@
    2.14  val _ = Markup.add_mode isabelle_processN YXML.output_markup;
    2.15  
    2.16  
    2.17 -(* commands *)
    2.18 +(* protocol commands *)
    2.19  
    2.20  local
    2.21  
    2.22 @@ -47,16 +46,18 @@
    2.23  
    2.24  in
    2.25  
    2.26 -fun add_command name cmd =
    2.27 +fun protocol_command name cmd =
    2.28    Synchronized.change commands (fn cmds =>
    2.29     (if not (Symtab.defined cmds name) then ()
    2.30      else warning ("Redefining Isabelle process command " ^ quote name);
    2.31      Symtab.update (name, cmd) cmds));
    2.32  
    2.33 -fun command name args =
    2.34 +fun run_command name args =
    2.35    (case Symtab.lookup (Synchronized.value commands) name of
    2.36      NONE => error ("Undefined Isabelle process command " ^ quote name)
    2.37 -  | SOME cmd => cmd args);
    2.38 +  | SOME cmd =>
    2.39 +      (Runtime.debugging cmd args handle exn =>
    2.40 +        error ("Isabelle process protocol failure: " ^ name ^ "\n" ^ ML_Compiler.exn_message exn)));
    2.41  
    2.42  end;
    2.43  
    2.44 @@ -145,11 +146,6 @@
    2.45      NONE => raise Runtime.TERMINATE
    2.46    | SOME line => map (read_chunk channel) (space_explode "," line));
    2.47  
    2.48 -fun run_command name args =
    2.49 -  Runtime.debugging (command name) args
    2.50 -    handle exn =>
    2.51 -      error ("Isabelle process command failure: " ^ name ^ "\n" ^ ML_Compiler.exn_message exn);
    2.52 -
    2.53  in
    2.54  
    2.55  fun loop channel =