--- a/src/Pure/PIDE/protocol.ML Wed Feb 03 20:18:34 2021 +0100
+++ b/src/Pure/PIDE/protocol.ML Sun Feb 07 12:30:52 2021 +0100
@@ -8,27 +8,27 @@
struct
val _ =
- Isabelle_Process.protocol_command "Prover.echo"
+ Protocol_Command.define "Prover.echo"
(fn args => List.app writeln args);
val _ =
- Isabelle_Process.protocol_command "Prover.stop"
+ Protocol_Command.define "Prover.stop"
(fn rc :: msgs =>
(List.app Output.system_message msgs;
- raise Isabelle_Process.STOP (Value.parse_int rc)));
+ raise Protocol_Command.STOP (Value.parse_int rc)));
val _ =
- Isabelle_Process.protocol_command "Prover.options"
+ Protocol_Command.define "Prover.options"
(fn [options_yxml] =>
(Options.set_default (Options.decode (YXML.parse_body options_yxml));
Isabelle_Process.init_options_interactive ()));
val _ =
- Isabelle_Process.protocol_command "Prover.init_session"
+ Protocol_Command.define "Prover.init_session"
(fn [yxml] => Resources.init_session_yxml yxml);
val _ =
- Isabelle_Process.protocol_command "Document.define_blob"
+ Protocol_Command.define "Document.define_blob"
(fn [digest, content] => Document.change_state (Document.define_blob digest content));
fun decode_command id name parents_xml blobs_xml toks_xml sources : Document.command =
@@ -63,7 +63,7 @@
Output.protocol_message Markup.commands_accepted [XML.Text (space_implode "," ids)];
val _ =
- Isabelle_Process.protocol_command "Document.define_command"
+ Protocol_Command.define "Document.define_command"
(fn id :: name :: parents :: blobs :: toks :: sources =>
let
val command =
@@ -73,7 +73,7 @@
in commands_accepted [id] end);
val _ =
- Isabelle_Process.protocol_command "Document.define_commands"
+ Protocol_Command.define "Document.define_commands"
(fn args =>
let
fun decode arg =
@@ -89,15 +89,15 @@
in commands_accepted (map (Value.print_int o #command_id) commands) end);
val _ =
- Isabelle_Process.protocol_command "Document.discontinue_execution"
+ Protocol_Command.define "Document.discontinue_execution"
(fn [] => Execution.discontinue ());
val _ =
- Isabelle_Process.protocol_command "Document.cancel_exec"
+ Protocol_Command.define "Document.cancel_exec"
(fn [exec_id] => Execution.cancel (Document_ID.parse exec_id));
val _ =
- Isabelle_Process.protocol_command "Document.update"
+ Protocol_Command.define "Document.update"
(Future.task_context "Document.update" (Future.new_group NONE)
(fn old_id_string :: new_id_string :: consolidate_yxml :: edits_yxml =>
Document.change_state (fn state =>
@@ -150,7 +150,7 @@
in Document.start_execution state' end)));
val _ =
- Isabelle_Process.protocol_command "Document.remove_versions"
+ Protocol_Command.define "Document.remove_versions"
(fn [versions_yxml] => Document.change_state (fn state =>
let
val versions =
@@ -161,17 +161,17 @@
in state1 end));
val _ =
- Isabelle_Process.protocol_command "Document.dialog_result"
+ Protocol_Command.define "Document.dialog_result"
(fn [serial, result] =>
Active.dialog_result (Value.parse_int serial) result
handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn);
val _ =
- Isabelle_Process.protocol_command "ML_Heap.full_gc"
+ Protocol_Command.define "ML_Heap.full_gc"
(fn [] => ML_Heap.full_gc ());
val _ =
- Isabelle_Process.protocol_command "ML_Heap.share_common_data"
+ Protocol_Command.define "ML_Heap.share_common_data"
(fn [] => ML_Heap.share_common_data ());
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/protocol_command.ML Sun Feb 07 12:30:52 2021 +0100
@@ -0,0 +1,47 @@
+(* Title: Pure/PIDE/protocol_command.ML
+ Author: Makarius
+
+Protocol commands.
+*)
+
+signature PROTOCOL_COMMAND =
+sig
+ exception STOP of int
+ val is_protocol_exn: exn -> bool
+ val define: string -> (string list -> unit) -> unit
+ val run: string -> string list -> unit
+end;
+
+structure Protocol_Command: PROTOCOL_COMMAND =
+struct
+
+exception STOP of int;
+
+val is_protocol_exn = fn STOP _ => true | _ => false;
+
+local
+
+val commands =
+ Synchronized.var "Protocol_Command.commands"
+ (Symtab.empty: (string list -> unit) Symtab.table);
+
+in
+
+fun define name cmd =
+ Synchronized.change commands (fn cmds =>
+ (if not (Symtab.defined cmds name) then ()
+ else warning ("Redefining Isabelle protocol command " ^ quote name);
+ Symtab.update (name, cmd) cmds));
+
+fun run name args =
+ (case Symtab.lookup (Synchronized.value commands) name of
+ NONE => error ("Undefined Isabelle protocol command " ^ quote name)
+ | SOME cmd =>
+ (Runtime.exn_trace_system (fn () => cmd args)
+ handle exn =>
+ if is_protocol_exn exn then Exn.reraise exn
+ else error ("Isabelle protocol command failure: " ^ quote name)));
+
+end;
+
+end;
--- a/src/Pure/ROOT.ML Wed Feb 03 20:18:34 2021 +0100
+++ b/src/Pure/ROOT.ML Sun Feb 07 12:30:52 2021 +0100
@@ -292,6 +292,7 @@
ML_file "Proof/extraction.ML";
(*Isabelle system*)
+ML_file "PIDE/protocol_command.ML";
ML_file "System/bash.ML";
ML_file "System/isabelle_system.ML";
@@ -354,4 +355,3 @@
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
ML_file "Tools/generated_files.ML"
-
--- a/src/Pure/System/isabelle_process.ML Wed Feb 03 20:18:34 2021 +0100
+++ b/src/Pure/System/isabelle_process.ML Sun Feb 07 12:30:52 2021 +0100
@@ -7,8 +7,6 @@
signature ISABELLE_PROCESS =
sig
val is_active: unit -> bool
- exception STOP of int
- val protocol_command: string -> (string list -> unit) -> unit
val reset_tracing: Document_ID.exec -> unit
val crashes: exn list Synchronized.var
val init_options: unit -> unit
@@ -33,38 +31,6 @@
val protocol_modes2 = [isabelle_processN, Pretty.symbolicN];
-(* protocol commands *)
-
-exception STOP of int;
-
-val is_protocol_exn = fn STOP _ => true | _ => false;
-
-local
-
-val commands =
- Synchronized.var "Isabelle_Process.commands"
- (Symtab.empty: (string list -> unit) Symtab.table);
-
-in
-
-fun protocol_command name cmd =
- Synchronized.change commands (fn cmds =>
- (if not (Symtab.defined cmds name) then ()
- 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 protocol command " ^ quote name)
- | SOME cmd =>
- (Runtime.exn_trace_system (fn () => cmd args)
- handle exn =>
- if is_protocol_exn exn then Exn.reraise exn
- else error ("Isabelle protocol command failure: " ^ quote name)));
-
-end;
-
-
(* restricted tracing messages *)
val tracing_messages =
@@ -192,11 +158,11 @@
let
val _ =
(case Byte_Message.read_message in_stream of
- NONE => raise STOP 0
+ NONE => raise Protocol_Command.STOP 0
| SOME [] => Output.system_message "Isabelle process: no input"
- | SOME (name :: args) => run_command name args)
+ | SOME (name :: args) => Protocol_Command.run name args)
handle exn =>
- if is_protocol_exn exn then Exn.reraise exn
+ if Protocol_Command.is_protocol_exn exn then Exn.reraise exn
else (Runtime.exn_system_message exn handle crash => recover crash);
in protocol_loop () end;
@@ -219,7 +185,7 @@
val _ = Options.reset_default ();
in
(case result of
- Exn.Exn (STOP rc) => if rc = 0 then () else exit rc
+ Exn.Exn (Protocol_Command.STOP rc) => if rc = 0 then () else exit rc
| _ => Exn.release result)
end);
--- a/src/Pure/System/scala.ML Wed Feb 03 20:18:34 2021 +0100
+++ b/src/Pure/System/scala.ML Sun Feb 07 12:30:52 2021 +0100
@@ -28,7 +28,7 @@
Synchronized.var "Scala.results" (Symtab.empty: string Exn.result Symtab.table);
val _ =
- Isabelle_Process.protocol_command "Scala.result"
+ Protocol_Command.define "Scala.result"
(fn [id, tag, res] =>
let
val result =
--- a/src/Pure/Tools/build.ML Wed Feb 03 20:18:34 2021 +0100
+++ b/src/Pure/Tools/build.ML Sun Feb 07 12:30:52 2021 +0100
@@ -50,7 +50,7 @@
(* build session *)
val _ =
- Isabelle_Process.protocol_command "build_session"
+ Protocol_Command.define "build_session"
(fn [resources_yxml, args_yxml] =>
let
val _ = Resources.init_session_yxml resources_yxml;
--- a/src/Pure/Tools/debugger.ML Wed Feb 03 20:18:34 2021 +0100
+++ b/src/Pure/Tools/debugger.ML Sun Feb 07 12:30:52 2021 +0100
@@ -243,7 +243,7 @@
(** protocol commands **)
val _ =
- Isabelle_Process.protocol_command "Debugger.init"
+ Protocol_Command.define "Debugger.init"
(fn [] =>
(init_input ();
PolyML.DebuggerInterface.setOnBreakPoint
@@ -256,15 +256,15 @@
else ()))));
val _ =
- Isabelle_Process.protocol_command "Debugger.exit"
+ Protocol_Command.define "Debugger.exit"
(fn [] => (PolyML.DebuggerInterface.setOnBreakPoint NONE; exit_input ()));
val _ =
- Isabelle_Process.protocol_command "Debugger.break"
+ Protocol_Command.define "Debugger.break"
(fn [b] => set_break (Value.parse_bool b));
val _ =
- Isabelle_Process.protocol_command "Debugger.breakpoint"
+ Protocol_Command.define "Debugger.breakpoint"
(fn [node_name, id0, breakpoint0, breakpoint_state0] =>
let
val id = Value.parse_int id0;
@@ -289,7 +289,7 @@
end);
val _ =
- Isabelle_Process.protocol_command "Debugger.input"
+ Protocol_Command.define "Debugger.input"
(fn thread_name :: msg => input thread_name msg);
end;
--- a/src/Pure/Tools/print_operation.ML Wed Feb 03 20:18:34 2021 +0100
+++ b/src/Pure/Tools/print_operation.ML Sun Feb 07 12:30:52 2021 +0100
@@ -27,7 +27,7 @@
|> map (fn (x, (y, _)) => (x, y)) |> rev
|> let open XML.Encode in list (pair string string) end);
-val _ = Isabelle_Process.protocol_command "print_operations" (fn [] => report ());
+val _ = Protocol_Command.define "print_operations" (fn [] => report ());
in
--- a/src/Pure/Tools/simplifier_trace.ML Wed Feb 03 20:18:34 2021 +0100
+++ b/src/Pure/Tools/simplifier_trace.ML Sun Feb 07 12:30:52 2021 +0100
@@ -400,7 +400,7 @@
trace_apply = simp_apply})
val _ =
- Isabelle_Process.protocol_command "Simplifier_Trace.reply"
+ Protocol_Command.define "Simplifier_Trace.reply"
(fn [serial_string, reply] =>
let
val serial = Value.parse_int serial_string