src/Pure/ML-Systems/polyml_common.ML
author wenzelm
Mon Mar 24 18:35:46 2008 +0100 (2008-03-24 ago)
changeset 26380 5d368eb42c11
parent 26220 d34b68c21f9a
child 26474 94735cff132c
permissions -rw-r--r--
removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1);
moved use_text/file to polyml_old_compiler4.ML;
PolyML.onEntry: no longer evaluate command line;
     1 (*  Title:      Pure/ML-Systems/polyml_common.ML
     2     ID:         $Id$
     3 
     4 Compatibility file for Poly/ML -- common part for 4.x and 5.x.
     5 *)
     6 
     7 use "ML-Systems/exn.ML";
     8 if List.exists (fn s => s = "Universal") (PolyML.Compiler.structureNames ()) then ()
     9 else use "ML-Systems/universal.ML";
    10 use "ML-Systems/multithreading.ML";
    11 use "ML-Systems/time_limit.ML";
    12 use "ML-Systems/system_shell.ML";
    13 
    14 
    15 
    16 (** ML system and platform related **)
    17 
    18 (* Compiler options *)
    19 
    20 val ml_system_fix_ints = false;
    21 
    22 PolyML.Compiler.printInAlphabeticalOrder := false;
    23 PolyML.Compiler.maxInlineSize := 80;
    24 
    25 
    26 (* old Poly/ML emulation *)
    27 
    28 local
    29   val orig_exit = exit;
    30 in
    31   open PolyML;
    32   val exit = orig_exit;
    33   fun quit () = exit 0;
    34 end;
    35 
    36 
    37 (* restore old-style character / string functions *)
    38 
    39 val ord = SML90.ord;
    40 val chr = SML90.chr;
    41 val explode = SML90.explode;
    42 val implode = SML90.implode;
    43 
    44 
    45 (* compiler-independent timing functions *)
    46 
    47 fun start_timing () =
    48   let val CPUtimer = Timer.startCPUTimer();
    49       val time = Timer.checkCPUTimer(CPUtimer)
    50   in  (CPUtimer,time)  end;
    51 
    52 fun end_timing (CPUtimer, {sys,usr}) =
    53   let open Time  (*...for Time.toString, Time.+ and Time.- *)
    54       val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
    55   in  "User " ^ toString (usr2-usr) ^
    56       "  All "^ toString (sys2-sys + usr2-usr) ^
    57       " secs"
    58       handle Time => ""
    59   end;
    60 
    61 fun check_timer timer =
    62   let
    63     val {sys, usr} = Timer.checkCPUTimer timer;
    64     val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
    65   in (sys, usr, gc) end;
    66 
    67 
    68 (* prompts *)
    69 
    70 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
    71 
    72 
    73 (* toplevel pretty printing (see also Pure/pure_setup.ML) *)
    74 
    75 fun make_pp _ pprint (str, blk, brk, en) _ _ obj =
    76   pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
    77     fn () => brk (99999, 0), en);
    78 
    79 (*print depth*)
    80 local
    81   val depth = ref 10;
    82 in
    83   fun get_print_depth () = ! depth;
    84   fun print_depth n = (depth := n; PolyML.print_depth n);
    85 end;
    86 
    87 
    88 
    89 (** interrupts **)
    90 
    91 exception Interrupt = SML90.Interrupt;
    92 
    93 local
    94 
    95 val sig_int = 2;
    96 val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
    97 
    98 val _ = Signal.signal (sig_int, default_handler);
    99 val _ = PolyML.onEntry (fn () => (Signal.signal (sig_int, default_handler); ()));
   100 
   101 fun change_signal new_handler f x =
   102   let
   103     (*RACE wrt. other signals!*)
   104     val old_handler = Signal.signal (sig_int, new_handler);
   105     val result = Exn.capture (f old_handler) x;
   106     val _ = Signal.signal (sig_int, old_handler);
   107   in Exn.release result end;
   108 
   109 in
   110 
   111 fun interruptible f = change_signal default_handler (fn _ => f);
   112 
   113 fun uninterruptible f =
   114   change_signal Signal.SIG_IGN
   115     (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
   116 
   117 end;
   118 
   119 
   120 
   121 (** OS related **)
   122 
   123 (* Posix patches *)
   124 
   125 (*This extension of the Poly/ML Signal structure is only necessary
   126   because in SML/NJ, types Posix.Signal.signal and Signals.signal differ.*)
   127 structure IsaSignal =
   128 struct
   129   open Signal
   130   val usr1 = Posix.Signal.usr1
   131   val usr2 = Posix.Signal.usr2
   132   val alrm = Posix.Signal.alrm
   133   val chld = Posix.Signal.chld
   134   val cont = Posix.Signal.cont
   135   val int  = Posix.Signal.int
   136   val quit = Posix.Signal.quit
   137 end;
   138 
   139 
   140 (* current directory *)
   141 
   142 val cd = OS.FileSys.chDir;
   143 val pwd = OS.FileSys.getDir;
   144 
   145 
   146 (*Convert a process ID to a decimal string (chiefly for tracing)*)
   147 fun string_of_pid pid =
   148   Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid));
   149 
   150 
   151 (* getenv *)
   152 
   153 fun getenv var =
   154   (case OS.Process.getEnv var of
   155     NONE => ""
   156   | SOME txt => txt);
   157 
   158 
   159 (* profile execution *)
   160 
   161 fun profile 0 f x = f x
   162   | profile n f x =
   163       let
   164         val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
   165         val res = Exn.capture f x;
   166         val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
   167       in Exn.release res end;
   168