main command loops are supposed to be uninterruptible -- no special treatment here;
--- 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);