src/Pure/System/session.ML

--- a/src/Pure/System/session.ML	Wed May 22 08:46:39 2013 +0200
+++ b/src/Pure/System/session.ML	Wed May 22 14:10:45 2013 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/System/session.ML
     Author:     Makarius
 
-Session management -- internal state of logic images (not thread-safe).
+Session management -- internal state of logic images.
 *)
 
 signature SESSION =
@@ -11,12 +11,14 @@
   val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     string -> string * string -> bool * string -> bool -> unit
   val finish: unit -> unit
+  val protocol_handler: string -> unit
+  val init_protocol_handlers: unit -> unit
 end;
 
 structure Session: SESSION =
 struct
 
-(* session state *)
+(** session identification -- not thread-safe **)
 
 val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"};
 val session_finished = Unsynchronized.ref false;
@@ -58,4 +60,20 @@
   Event_Timer.shutdown ();
   session_finished := true);
 
+
+(** protocol handlers **)
+
+val protocol_handlers = Synchronized.var "protocol_handlers" ([]: string list);
+
+fun protocol_handler name =
+  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 () =
+  Synchronized.value protocol_handlers
+  |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) "");
+
 end;