src/Pure/ML-Systems/polyml.ML
changeset 16374 f4b7cf8975af
parent 16266 7a6616be8712
child 16453 af3afdbd09ea
equal deleted inserted replaced
16373:9d020423093b 16374:f4b7cf8975af
     4     Copyright   1991  University of Cambridge
     4     Copyright   1991  University of Cambridge
     5 
     5 
     6 Compatibility file for Poly/ML (version 4.0, 4.1, 4.1.x).
     6 Compatibility file for Poly/ML (version 4.0, 4.1, 4.1.x).
     7 *)
     7 *)
     8 
     8 
     9 (** ML system related **)
     9 (** ML system and platform related **)
       
    10 
       
    11 (* cygwin *)
       
    12 
       
    13 val cygwin_platform =
       
    14   let val n = size ml_platform
       
    15   in n >= 6 andalso String.substring (ml_platform, n - 6, 6) = "cygwin" end;
       
    16 
       
    17 fun if_cygwin f x = if cygwin_platform then f x else ();
       
    18 fun unless_cygwin f x = if not cygwin_platform then f x else ();
       
    19 
    10 
    20 
    11 (* old Poly/ML emulation *)
    21 (* old Poly/ML emulation *)
    12 
    22 
    13 local
    23 local
    14   val orig_exit = exit;
    24   val orig_exit = exit;
    32 use "ML-Systems/cpu-timer-basis.ML";
    42 use "ML-Systems/cpu-timer-basis.ML";
    33 
    43 
    34 
    44 
    35 (* bounded time execution *)
    45 (* bounded time execution *)
    36 
    46 
    37 use "ML-Systems/polyml-time-limit.ML";
    47 unless_cygwin
       
    48   use "ML-Systems/polyml-time-limit.ML";
    38 
    49 
    39 
    50 
    40 (* prompts *)
    51 (* prompts *)
    41 
    52 
    42 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
    53 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
   166 *)
   177 *)
   167 
   178 
   168 val profiling: int->unit =
   179 val profiling: int->unit =
   169      RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler;
   180      RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler;
   170 
   181 
   171 structure OriginalPosix = Posix;
   182 unless_cygwin
   172 structure OriginalIO = Posix.IO;
   183   use "ML-Systems/polyml-posix.ML";
   173 
       
   174 structure Posix =
       
   175 struct
       
   176   open OriginalPosix
       
   177   structure IO =
       
   178   struct
       
   179   open OriginalIO
       
   180   val mkTextReader = mkReader
       
   181   val mkTextWriter = mkWriter
       
   182   end;
       
   183 end;
       
   184 
       
   185 (*This extension of the Poly/ML Signal structure is only necessary
       
   186   because in SML/NJ, types Posix.Signal.signal and Signals.signal differ.*)
       
   187 structure IsaSignal =
       
   188 struct
       
   189   open Signal
       
   190   val usr1 = Posix.Signal.usr1
       
   191   val usr2 = Posix.Signal.usr2
       
   192 end;