main command loops are supposed to be uninterruptible -- no special treatment here;
authorwenzelm
Thu Sep 09 18:00:16 2010 +0200 (2010-09-09 ago)
changeset 39234d76a2fd129b5
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
     1.1 --- a/src/Pure/System/isabelle_process.ML	Thu Sep 09 17:38:45 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Thu Sep 09 18:00:16 2010 +0200
     1.3 @@ -117,7 +117,7 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -(* protocol loop *)
     1.8 +(* protocol loop -- uninterruptible *)
     1.9  
    1.10  val crashes = Unsynchronized.ref ([]: exn list);
    1.11  
     2.1 --- a/src/Pure/System/isar.ML	Thu Sep 09 17:38:45 2010 +0200
     2.2 +++ b/src/Pure/System/isar.ML	Thu Sep 09 18:00:16 2010 +0200
     2.3 @@ -111,7 +111,7 @@
     2.4    | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
     2.5  
     2.6  
     2.7 -(* toplevel loop *)
     2.8 +(* toplevel loop -- uninterruptible *)
     2.9  
    2.10  val crashes = Unsynchronized.ref ([]: exn list);
    2.11