# HG changeset patch
# User wenzelm
# Date 1284048016 -7200
# Node ID d76a2fd129b521fe7eb92f9d49b2817c7525a572
# Parent  9a0c67d4517a73634a32b171edabc7c94352aa99
main command loops are supposed to be uninterruptible -- no special treatment here;

diff -r 9a0c67d4517a -r d76a2fd129b5 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Thu Sep 09 17:38:45 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Thu Sep 09 18:00:16 2010 +0200
@@ -117,7 +117,7 @@
 end;
 
 
-(* protocol loop *)
+(* protocol loop -- uninterruptible *)
 
 val crashes = Unsynchronized.ref ([]: exn list);
 
diff -r 9a0c67d4517a -r d76a2fd129b5 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Thu Sep 09 17:38:45 2010 +0200
+++ b/src/Pure/System/isar.ML	Thu Sep 09 18:00:16 2010 +0200
@@ -111,7 +111,7 @@
   | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
 
 
-(* toplevel loop *)
+(* toplevel loop -- uninterruptible *)
 
 val crashes = Unsynchronized.ref ([]: exn list);