src/Pure/PIDE/session.ML
changeset 72156 065dcd80293e
parent 72098 8c547eac8381
child 72309 564012e31db1
--- 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;