src/Pure/ML-Systems/smlnj.ML
author wenzelm
Thu Jun 04 17:31:38 2009 +0200 (2009-06-04)
changeset 31427 5a07cc86675d
parent 31321 fe786d4633b9
child 31686 e54ae15335a1
permissions -rw-r--r--
reraise exceptions to preserve original position (ML system specific);
     1 (*  Title:      Pure/ML-Systems/smlnj.ML
     2 
     3 Compatibility file for Standard ML of New Jersey 110 or later.
     4 *)
     5 
     6 exception Interrupt;
     7 fun reraise exn = raise exn;
     8 
     9 use "ML-Systems/proper_int.ML";
    10 use "ML-Systems/overloading_smlnj.ML";
    11 use "ML-Systems/exn.ML";
    12 use "ML-Systems/universal.ML";
    13 use "ML-Systems/thread_dummy.ML";
    14 use "ML-Systems/multithreading.ML";
    15 use "ML-Systems/system_shell.ML";
    16 use "ML-Systems/ml_name_space.ML";
    17 use "ML-Systems/ml_pretty.ML";
    18 use "ML-Systems/use_context.ML";
    19 
    20 
    21 (*low-level pointer equality*)
    22 
    23 CM.autoload "$smlnj/init/init.cmi";
    24 val pointer_eq = InlineT.ptreql;
    25 
    26 
    27 (* restore old-style character / string functions *)
    28 
    29 val ord     = mk_int o SML90.ord;
    30 val chr     = SML90.chr o dest_int;
    31 val explode = SML90.explode;
    32 val implode = SML90.implode;
    33 
    34 
    35 (* New Jersey ML parameters *)
    36 
    37 val _ =
    38  (Control.Print.printLength := 1000;
    39   Control.Print.printDepth := 350;
    40   Control.Print.stringDepth := 250;
    41   Control.Print.signatures := 2;
    42   Control.MC.matchRedundantError := false);
    43 
    44 
    45 (* Poly/ML emulation *)
    46 
    47 val exit = exit o dest_int;
    48 fun quit () = exit 0;
    49 
    50 (*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
    51 local
    52   val depth = ref (10: int);
    53 in
    54   fun get_print_depth () = ! depth;
    55   fun print_depth n =
    56    (depth := n;
    57     Control.Print.printDepth := dest_int n div 2;
    58     Control.Print.printLength := dest_int n);
    59 end;
    60 
    61 
    62 (* compiler-independent timing functions *)
    63 
    64 fun start_timing () =
    65   let
    66     val timer = Timer.startCPUTimer ();
    67     val time = Timer.checkCPUTimer timer;
    68   in (timer, time) end;
    69 
    70 fun end_timing (timer, {sys, usr}) =
    71   let
    72     open Time;  (*...for Time.toString, Time.+ and Time.- *)
    73     val {sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
    74     val user = usr2 - usr;
    75     val all = user + sys2 - sys;
    76     val message = "User " ^ toString user ^ "  All "^ toString all ^ " secs" handle Time => "";
    77   in {message = message, user = user, all = all} end;
    78 
    79 fun check_timer timer =
    80   let
    81     val {sys, usr} = Timer.checkCPUTimer timer;
    82     val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
    83   in (sys, usr, gc) end;
    84 
    85 
    86 (*prompts*)
    87 fun ml_prompts p1 p2 =
    88   (Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
    89 
    90 (*dummy implementation*)
    91 fun profile (n: int) f x = f x;
    92 
    93 (*dummy implementation*)
    94 fun exception_trace f = f ();
    95 
    96 
    97 (* ML command execution *)
    98 
    99 fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
   100   let
   101     val ref out_orig = Control.Print.out;
   102 
   103     val out_buffer = ref ([]: string list);
   104     val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
   105     fun output () =
   106       let val str = implode (rev (! out_buffer))
   107       in String.substring (str, 0, Int.max (0, size str - 1)) end;
   108   in
   109     Control.Print.out := out;
   110     Backend.Interact.useStream (TextIO.openString (tune_source txt)) handle exn =>
   111       (Control.Print.out := out_orig;
   112         error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
   113     Control.Print.out := out_orig;
   114     if verbose then print (output ()) else ()
   115   end;
   116 
   117 fun use_file context verbose name =
   118   let
   119     val instream = TextIO.openIn name;
   120     val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
   121   in use_text context (1, name) verbose txt end;
   122 
   123 fun forget_structure _ = ();
   124 
   125 
   126 (* toplevel pretty printing *)
   127 
   128 fun ml_pprint pps =
   129   let
   130     fun str "" = ()
   131       | str s = PrettyPrint.string pps s;
   132     fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
   133           (str bg; PrettyPrint.openHOVBox pps (PrettyPrint.Rel (dest_int ind));
   134             List.app pprint prts; PrettyPrint.closeBox pps; str en)
   135       | pprint (ML_Pretty.String (s, _)) = str s
   136       | pprint (ML_Pretty.Break (false, wd)) = PrettyPrint.break pps {nsp = dest_int wd, offset = 0}
   137       | pprint (ML_Pretty.Break (true, _)) = PrettyPrint.newline pps;
   138   in pprint end;
   139 
   140 fun toplevel_pp context path pp =
   141   use_text context (1, "pp") false
   142     ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"")  path) ^
   143       "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
   144 
   145 
   146 
   147 (** interrupts **)
   148 
   149 local
   150 
   151 fun change_signal new_handler f x =
   152   let
   153     val old_handler = Signals.setHandler (Signals.sigINT, new_handler);
   154     val result = Exn.capture (f old_handler) x;
   155     val _ = Signals.setHandler (Signals.sigINT, old_handler);
   156   in Exn.release result end;
   157 
   158 in
   159 
   160 fun interruptible (f: 'a -> 'b) x =
   161   let
   162     val result = ref (Exn.Exn Interrupt: 'b Exn.result);
   163     val old_handler = Signals.inqHandler Signals.sigINT;
   164   in
   165     SMLofNJ.Cont.callcc (fn cont =>
   166       (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => cont));
   167         result := Exn.capture f x));
   168     Signals.setHandler (Signals.sigINT, old_handler);
   169     Exn.release (! result)
   170   end;
   171 
   172 fun uninterruptible f =
   173   change_signal Signals.IGNORE
   174     (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
   175 
   176 end;
   177 
   178 
   179 (* basis library fixes *)
   180 
   181 structure TextIO =
   182 struct
   183   open TextIO;
   184   fun inputLine is = TextIO.inputLine is
   185     handle IO.Io _ => raise Interrupt;
   186 end;
   187 
   188 
   189 
   190 (** OS related **)
   191 
   192 (* current directory *)
   193 
   194 val cd = OS.FileSys.chDir;
   195 val pwd = OS.FileSys.getDir;
   196 
   197 
   198 (* system command execution *)
   199 
   200 val system_out = (fn (output, rc) => (output, mk_int rc)) o system_out;
   201 
   202 
   203 (*Convert a process ID to a decimal string (chiefly for tracing)*)
   204 fun process_id pid =
   205   Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ())));
   206 
   207 
   208 (* getenv *)
   209 
   210 fun getenv var =
   211   (case OS.Process.getEnv var of
   212     NONE => ""
   213   | SOME txt => txt);