main command loops are supposed to be uninterruptible -- no special treatment here;
authorwenzelm
Thu, 09 Sep 2010 18:00:16 +0200
changeset 39234 d76a2fd129b5
parent 39233 9a0c67d4517a
child 39235 cda88e68106d
main command loops are supposed to be uninterruptible -- no special treatment here;
src/Pure/System/isabelle_process.ML
src/Pure/System/isar.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);
 
--- 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);