--- a/src/Pure/PIDE/session.ML Sat Apr 09 20:14:00 2016 +0200
+++ b/src/Pure/PIDE/session.ML Sat Apr 09 20:18:15 2016 +0200
@@ -80,14 +80,18 @@
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));
+ 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 () =
- Synchronized.value protocol_handlers
- |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) []);
+ if Thread_Data.is_virtual then ()
+ else
+ Synchronized.value protocol_handlers
+ |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) []);
end;