--- 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"
--- 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)];
--- 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")
--- 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 =
--- 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;
--- 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()
--- 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 ());
--- 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 =
--- 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 =
--- 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,