# HG changeset patch
# User wenzelm
# Date 1373481879 -7200
# Node ID bd94e26e43887629992a0fae73f4e04ab71070d7
# Parent  a9ae6534dc5cff0a8891f7188c907780cbc3c545
retain main thread for protocol loop -- no access to raw ML toplevel;

diff -r a9ae6534dc5c -r bd94e26e4388 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Jul 10 20:19:51 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed Jul 10 20:44:39 2013 +0200
@@ -211,9 +211,8 @@
   [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN, Graph_Display.active_graphN];
 val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN];
 
-fun init rendezvous = ignore (Simple_Thread.fork false (fn () =>
+val init = uninterruptible (fn _ => fn rendezvous =>
   let
-    val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
     val _ = Output.physical_stderr Symbol.STX;
 
     val _ = Printer.show_markup_default := true;
@@ -225,7 +224,7 @@
     val channel = rendezvous ();
     val _ = init_channels channel;
     val _ = Session.init_protocol_handlers ();
-  in loop channel end));
+  in loop channel end);
 
 fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
 fun init_socket name = init (fn () => System_Channel.socket_rendezvous name);