# HG changeset patch
# User wenzelm
# Date 1597491454 -7200
# Node ID 065dcd80293e1c39f272ba1ec557813ab641d3e2
# Parent  837b86b214d315750adb5e70df9cfcbdf3363e88
provide protocol handlers via isabelle_system_service;

diff -r 837b86b214d3 -r 065dcd80293e etc/settings
--- a/etc/settings	Sat Aug 15 13:36:42 2020 +0200
+++ b/etc/settings	Sat Aug 15 13:37:34 2020 +0200
@@ -27,6 +27,11 @@
 
 isabelle_scala_service 'isabelle.Bibtex$File_Format'
 
+isabelle_scala_service 'isabelle.ML_Statistics$Protocol_Handler'
+isabelle_scala_service 'isabelle.Scala'
+isabelle_scala_service 'isabelle.Print_Operation$Handler'
+isabelle_scala_service 'isabelle.Simplifier_Trace$Handler'
+
 #paranoia settings -- avoid intrusion of alien options
 unset "_JAVA_OPTIONS"
 unset "JAVA_TOOL_OPTIONS"
diff -r 837b86b214d3 -r 065dcd80293e src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sat Aug 15 13:36:42 2020 +0200
+++ b/src/Pure/PIDE/markup.ML	Sat Aug 15 13:37:34 2020 +0200
@@ -213,7 +213,6 @@
   val commands_accepted: Properties.T
   val assign_update: Properties.T
   val removed_versions: Properties.T
-  val protocol_handler: string -> Properties.T
   val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
   val task_statistics: Properties.entry
@@ -680,8 +679,6 @@
 val assign_update = [(functionN, "assign_update")];
 val removed_versions = [(functionN, "removed_versions")];
 
-fun protocol_handler name = [(functionN, "protocol_handler"), (nameN, name)];
-
 fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
 
diff -r 837b86b214d3 -r 065dcd80293e src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sat Aug 15 13:36:42 2020 +0200
+++ b/src/Pure/PIDE/markup.scala	Sat Aug 15 13:37:34 2020 +0200
@@ -599,8 +599,6 @@
   object Loading_Theory extends Name_Function("loading_theory")
   object Build_Session_Finished extends Function("build_session_finished")
 
-  object Protocol_Handler extends Name_Function("protocol_handler")
-
   object Commands_Accepted extends Function("commands_accepted")
   object Assign_Update extends Function("assign_update")
   object Removed_Versions extends Function("removed_versions")
diff -r 837b86b214d3 -r 065dcd80293e src/Pure/PIDE/protocol_handlers.scala
--- a/src/Pure/PIDE/protocol_handlers.scala	Sat Aug 15 13:36:42 2020 +0200
+++ b/src/Pure/PIDE/protocol_handlers.scala	Sat Aug 15 13:37:34 2020 +0200
@@ -23,29 +23,16 @@
     def init(handler: Session.Protocol_Handler): State =
     {
       val name = handler.getClass.getName
-
-      val (handlers1, functions1) =
-        handlers.get(name) match {
-          case Some(old_handler) =>
-            Output.warning("Redefining protocol handler: " + name)
-            old_handler.exit()
-            (handlers - name, functions -- old_handler.functions.map(_._1))
-          case None => (handlers, functions)
+      try {
+        if (handlers.isDefinedAt(name)) error("Duplicate protocol handler: " + name)
+        else {
+          handler.init(session)
+          val dups = for ((a, _) <- handler.functions if functions.isDefinedAt(a)) yield a
+          if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
+          copy(handlers = handlers + (name -> handler), functions = functions ++ handler.functions)
         }
-
-      val (handlers2, functions2) =
-        try {
-          handler.init(session)
-
-          val dups = for ((a, _) <- handler.functions if functions1.isDefinedAt(a)) yield a
-          if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
-
-          (handlers1 + (name -> handler), functions1 ++ handler.functions)
-        }
-        catch {
-          case exn: Throwable => bad_handler(exn, name); (handlers1, functions1)
-        }
-      copy(handlers = handlers2, functions = functions2)
+      }
+      catch { case exn: Throwable => bad_handler(exn, name); this }
     }
 
     def init(name: String): State =
diff -r 837b86b214d3 -r 065dcd80293e src/Pure/PIDE/session.ML
--- a/src/Pure/PIDE/session.ML	Sat Aug 15 13:36:42 2020 +0200
+++ b/src/Pure/PIDE/session.ML	Sat Aug 15 13:37:34 2020 +0200
@@ -13,8 +13,6 @@
     (Path.T * Path.T) list -> Path.T -> string -> string * string -> bool -> unit
   val shutdown: unit -> unit
   val finish: unit -> unit
-  val protocol_handler: string -> unit
-  val init_protocol_handlers: unit -> unit
 end;
 
 structure Session: SESSION =
@@ -74,25 +72,4 @@
   update_keywords ();
   Synchronized.change session (apsnd (K true)));
 
-
-
-(** protocol handlers **)
-
-val protocol_handlers = Synchronized.var "protocol_handlers" ([]: string list);
-
-fun protocol_handler name =
-  if Thread_Data.is_virtual then ()
-  else
-    Synchronized.change protocol_handlers (fn handlers =>
-     (Output.try_protocol_message (Markup.protocol_handler name) [];
-      if not (member (op =) handlers name) then ()
-      else warning ("Redefining protocol handler: " ^ quote name);
-      update (op =) name handlers));
-
-fun init_protocol_handlers () =
-  if Thread_Data.is_virtual then ()
-  else
-    Synchronized.value protocol_handlers
-    |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) []);
-
 end;
diff -r 837b86b214d3 -r 065dcd80293e src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sat Aug 15 13:36:42 2020 +0200
+++ b/src/Pure/PIDE/session.scala	Sat Aug 15 13:37:34 2020 +0200
@@ -113,7 +113,7 @@
 
   type Protocol_Function = Prover.Protocol_Output => Boolean
 
-  abstract class Protocol_Handler
+  abstract class Protocol_Handler extends Isabelle_System.Service
   {
     def init(session: Session): Unit = {}
     def exit(): Unit = {}
@@ -369,9 +369,6 @@
   def init_protocol_handler(handler: Session.Protocol_Handler): Unit =
     protocol_handlers.init(handler)
 
-  def init_protocol_handler(name: String): Unit =
-    protocol_handlers.init(name)
-
 
   /* debugger */
 
@@ -484,9 +481,6 @@
           val handled = protocol_handlers.invoke(msg)
           if (!handled) {
             msg.properties match {
-              case Markup.Protocol_Handler(name) if prover.defined =>
-                init_protocol_handler(name)
-
               case Protocol.Command_Timing(props, state_id, timing) if prover.defined =>
                 command_timings.post(Session.Command_Timing(props))
                 val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
@@ -548,6 +542,13 @@
             case _ if output.is_init =>
               prover.get.options(file_formats.prover_options(session_options))
               prover.get.init_session(resources)
+
+              Isabelle_System.services.foreach(
+                {
+                  case handler: Session.Protocol_Handler => init_protocol_handler(handler)
+                  case _ =>
+                })
+
               phase = Session.Ready
               debugger.ready()
 
diff -r 837b86b214d3 -r 065dcd80293e src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Sat Aug 15 13:36:42 2020 +0200
+++ b/src/Pure/System/isabelle_process.ML	Sat Aug 15 13:37:34 2020 +0200
@@ -117,8 +117,6 @@
   Output.protocol_message
     (Markup.ML_statistics {pid = ML_Pid.get (), stats_dir = getenv "POLYSTATSDIR"}) [];
 
-val _ = Session.protocol_handler "isabelle.ML_Statistics$Protocol_Handler";
-
 in
 
 fun init_protocol modes = Thread_Attributes.uninterruptible (fn _ => fn (address, password) =>
@@ -204,8 +202,7 @@
       in protocol_loop () end;
 
     fun protocol () =
-     (Session.init_protocol_handlers ();
-      ml_statistics ();
+     (ml_statistics ();
       message Markup.initN [] [XML.Text (Session.welcome ())];
       protocol_loop ());
 
diff -r 837b86b214d3 -r 065dcd80293e src/Pure/System/scala.ML
--- a/src/Pure/System/scala.ML	Sat Aug 15 13:36:42 2020 +0200
+++ b/src/Pure/System/scala.ML	Sat Aug 15 13:37:34 2020 +0200
@@ -40,8 +40,6 @@
           | _ => raise Fail ("Bad tag: " ^ tag));
       in Synchronized.change results (Symtab.map_entry id (K result)) end);
 
-val _ = Session.protocol_handler "isabelle.Scala";
-
 in
 
 fun function name arg =
diff -r 837b86b214d3 -r 065dcd80293e src/Pure/Tools/print_operation.ML
--- a/src/Pure/Tools/print_operation.ML	Sat Aug 15 13:36:42 2020 +0200
+++ b/src/Pure/Tools/print_operation.ML	Sat Aug 15 13:37:34 2020 +0200
@@ -29,8 +29,6 @@
 
 val _ = Isabelle_Process.protocol_command "print_operations" (fn [] => report ());
 
-val _ = Session.protocol_handler "isabelle.Print_Operation$Handler";
-
 in
 
 fun register name description pr =
diff -r 837b86b214d3 -r 065dcd80293e src/Pure/Tools/simplifier_trace.ML
--- a/src/Pure/Tools/simplifier_trace.ML	Sat Aug 15 13:36:42 2020 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML	Sat Aug 15 13:37:34 2020 +0200
@@ -394,8 +394,6 @@
         end)
   end
 
-val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler"
-
 val _ = Theory.setup
   (Simplifier.set_trace_ops
     {trace_invoke = fn {depth, term} => recurse "Simplifier invoked" depth term,