avoid interference with running PIDE protocol;
authorwenzelm
Sat, 09 Apr 2016 20:18:15 +0200
changeset 62936 72e3811dad76
parent 62935 3c7a35c12e03
child 62937 d5e7a76ec1a6
avoid interference with running PIDE protocol;
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;