src/Pure/ML-Systems/polyml-4.0.ML
changeset 10517 b9f7adf3ff11
parent 10209 b24210573eca
child 10518 20d4899f5d48
equal deleted inserted replaced
10516:dc113303d101 10517:b9f7adf3ff11
    94 
    94 
    95 
    95 
    96 
    96 
    97 (** interrupts **)
    97 (** interrupts **)
    98 
    98 
       
    99 exception Interrupt;
       
   100 
    99 local
   101 local
   100 
   102 
   101 datatype 'a result =
   103 datatype 'a result =
   102   Result of 'a |
   104   Result of 'a |
   103   Exn of exn;
   105   Exn of exn;