src/Pure/ML-Systems/smlnj.ML
changeset 18790 418131f631fc
parent 18760 97aaecb84afe
child 21298 6d2306b2376d
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Thu Jan 26 20:17:54 2006 +0100
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Thu Jan 26 20:42:15 2006 +0100
     1.3 @@ -59,11 +59,6 @@
     1.4  | _ => use "ML-Systems/cpu-timer-gc.ML");
     1.5  
     1.6  
     1.7 -(* bounded time execution *)
     1.8 -
     1.9 -use "ML-Systems/smlnj-interrupt-timeout.ML";
    1.10 -
    1.11 -
    1.12  (*prompts*)
    1.13  fun ml_prompts p1 p2 =
    1.14    (Compiler.Control.primaryPrompt := p1; Compiler.Control.secondaryPrompt := p2);
    1.15 @@ -108,7 +103,6 @@
    1.16    end;
    1.17  
    1.18  
    1.19 -
    1.20  (** interrupts **)
    1.21  
    1.22  exception Interrupt;
    1.23 @@ -151,6 +145,12 @@
    1.24  | _ => ());
    1.25  
    1.26  
    1.27 +
    1.28 +(* bounded time execution *)
    1.29 +
    1.30 +use "ML-Systems/smlnj-interrupt-timeout.ML";
    1.31 +
    1.32 +
    1.33  (** Signal handling: emulation of the Poly/ML Signal structure. Note that types
    1.34      Posix.Signal.signal and Signals.signal differ **)
    1.35