# HG changeset patch
# User wenzelm
# Date 1612697452 -3600
# Node ID 3ab0cedaccadfa77381ec6a36e244de2a7e1f290
# Parent  49686e3b1909841cf58703d6162efdfcda8b0ec8
clarified modules: allow early definition of protocol commands;

diff -r 49686e3b1909 -r 3ab0cedaccad src/Pure/PIDE/protocol.ML
--- 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;
diff -r 49686e3b1909 -r 3ab0cedaccad src/Pure/PIDE/protocol_command.ML
--- /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;
diff -r 49686e3b1909 -r 3ab0cedaccad src/Pure/ROOT.ML
--- 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"
-
diff -r 49686e3b1909 -r 3ab0cedaccad src/Pure/System/isabelle_process.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);
 
diff -r 49686e3b1909 -r 3ab0cedaccad src/Pure/System/scala.ML
--- 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 =
diff -r 49686e3b1909 -r 3ab0cedaccad src/Pure/Tools/build.ML
--- 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;
diff -r 49686e3b1909 -r 3ab0cedaccad src/Pure/Tools/debugger.ML
--- 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;
diff -r 49686e3b1909 -r 3ab0cedaccad src/Pure/Tools/print_operation.ML
--- 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
 
diff -r 49686e3b1909 -r 3ab0cedaccad src/Pure/Tools/simplifier_trace.ML
--- 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