src/Pure/ML-Systems/multithreading_polyml.ML
changeset 39232 69c6d3e87660
parent 35023 16f9877abf0b
child 39576 48baf61cb888
     1.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Sep 09 11:05:52 2010 +0200
     1.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Thu Sep 09 17:20:27 2010 +0200
     1.3 @@ -148,7 +148,7 @@
     1.4        (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
     1.5  
     1.6      val result = Exn.capture (restore_attributes f) x;
     1.7 -    val was_timeout = (case result of Exn.Exn Exn.Interrupt => ! timeout | _ => false);
     1.8 +    val was_timeout = Exn.is_interrupt_exn result andalso ! timeout;
     1.9  
    1.10      val _ = Thread.interrupt watchdog handle Thread _ => ();
    1.11    in if was_timeout then raise TimeOut else Exn.release result end) ();
    1.12 @@ -209,7 +209,7 @@
    1.13          let val res =
    1.14            sync_wait (SOME orig_atts)
    1.15              (SOME (Time.+ (Time.now (), Time.fromMilliseconds 100))) cond lock
    1.16 -        in case res of Exn.Exn Exn.Interrupt => kill 10 | _ => () end;
    1.17 +        in if Exn.is_interrupt_exn res then kill 10 else () end;
    1.18  
    1.19      (*cleanup*)
    1.20      val output = read_file output_name handle IO.Io _ => "";
    1.21 @@ -217,7 +217,7 @@
    1.22      val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
    1.23      val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
    1.24      val _ = Thread.interrupt system_thread handle Thread _ => ();
    1.25 -    val rc = (case ! result of Signal => raise Exn.Interrupt | Result rc => rc);
    1.26 +    val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc);
    1.27    in (output, rc) end);
    1.28  
    1.29