src/Pure/ML-Systems/multithreading_polyml.ML
changeset 28443 de653f1ad78b
parent 28398 9aa3216e5f31
child 28465 db8667d84dd2
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Oct 01 12:00:01 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Oct 01 12:00:02 2008 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4          val result = Exn.capture (f orig_atts) x;
     1.5          val _ = restore ();
     1.6        in result end
     1.7 -      handle Interrupt => (restore (); Exn.Exn Interrupt))
     1.8 +      handle Exn.Interrupt => (restore (); Exn.Exn Exn.Interrupt))
     1.9    end;
    1.10  
    1.11  fun interruptible f = with_attributes regular_interrupts (fn _ => f);
    1.12 @@ -105,7 +105,7 @@
    1.13  
    1.14      (*RACE! timeout signal vs. external Interrupt*)
    1.15      val result = Exn.capture (restore_attributes f) x;
    1.16 -    val was_timeout = (case result of Exn.Exn Interrupt => ! timeout | _ => false);
    1.17 +    val was_timeout = (case result of Exn.Exn Exn.Interrupt => ! timeout | _ => false);
    1.18  
    1.19      val _ = Thread.interrupt watchdog handle Thread _ => ();
    1.20    in if was_timeout then raise TimeOut else Exn.release result end) ();
    1.21 @@ -165,7 +165,7 @@
    1.22      val _ = while ! result = Wait do
    1.23        restore_attributes (fn () =>
    1.24          (ConditionVar.waitUntil (result_cond, result_mutex, Time.now () + Time.fromMilliseconds 100); ())
    1.25 -          handle Interrupt => kill 10) ();
    1.26 +          handle Exn.Interrupt => kill 10) ();
    1.27  
    1.28      (*cleanup*)
    1.29      val output = read_file output_name handle IO.Io _ => "";
    1.30 @@ -173,7 +173,7 @@
    1.31      val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
    1.32      val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
    1.33      val _ = Thread.interrupt system_thread handle Thread _ => ();
    1.34 -    val rc = (case ! result of Signal => raise Interrupt | Result rc => rc);
    1.35 +    val rc = (case ! result of Signal => raise Exn.Interrupt | Result rc => rc);
    1.36    in (output, rc) end) ();
    1.37  
    1.38