# HG changeset patch
# User wenzelm
# Date 1460225895 -7200
# Node ID 72e3811dad762b3327ba740c87a63f35fa0c2836
# Parent  3c7a35c12e03048520af8d23bcef10e3afdbc2c7
avoid interference with running PIDE protocol;

diff -r 3c7a35c12e03 -r 72e3811dad76 src/Pure/PIDE/session.ML
--- 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;