src/Pure/ML-Systems/polyml_common.ML
author wenzelm
Sat Nov 27 16:29:53 2010 +0100 (2010-11-27 ago)
changeset 40748 591b6778d076
parent 40627 becf5d5187cc
child 41352 87adb55fb0fb
permissions -rw-r--r--
removed bash from ML system bootstrap, and past the Secure ML barrier;
     1 (*  Title:      Pure/ML-Systems/polyml_common.ML
     2 
     3 Compatibility file for Poly/ML -- common part for 5.x.
     4 *)
     5 
     6 exception Interrupt = SML90.Interrupt;
     7 
     8 use "General/exn.ML";
     9 
    10 if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ())
    11 then ()
    12 else use "ML-Systems/single_assignment_polyml.ML";
    13 
    14 use "ML-Systems/multithreading.ML";
    15 use "ML-Systems/time_limit.ML";
    16 use "General/timing.ML";
    17 use "ML-Systems/ml_pretty.ML";
    18 use "ML-Systems/use_context.ML";
    19 
    20 
    21 (** ML system and platform related **)
    22 
    23 val forget_structure = PolyML.Compiler.forgetStructure;
    24 
    25 val _ = PolyML.Compiler.forgetValue "isSome";
    26 val _ = PolyML.Compiler.forgetValue "getOpt";
    27 val _ = PolyML.Compiler.forgetValue "valOf";
    28 val _ = PolyML.Compiler.forgetValue "foldl";
    29 val _ = PolyML.Compiler.forgetValue "foldr";
    30 val _ = PolyML.Compiler.forgetValue "print";
    31 val _ = PolyML.Compiler.forgetValue "explode";
    32 
    33 
    34 (* Compiler options *)
    35 
    36 val ml_system_fix_ints = false;
    37 
    38 PolyML.Compiler.printInAlphabeticalOrder := false;
    39 PolyML.Compiler.maxInlineSize := 80;
    40 
    41 
    42 (* old Poly/ML emulation *)
    43 
    44 fun quit () = exit 0;
    45 
    46 
    47 (* restore old-style character / string functions *)
    48 
    49 val ord = SML90.ord;
    50 val chr = SML90.chr;
    51 val raw_explode = SML90.explode;
    52 val implode = SML90.implode;
    53 
    54 
    55 (* prompts *)
    56 
    57 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
    58 
    59 
    60 (* toplevel printing *)
    61 
    62 local
    63   val depth = ref 10;
    64 in
    65   fun get_print_depth () = ! depth;
    66   fun print_depth n = (depth := n; PolyML.print_depth n);
    67 end;
    68 
    69 val error_depth = PolyML.error_depth;
    70 
    71 val ml_make_string = "PolyML.makestring";
    72 
    73 
    74 
    75 (** interrupts **)
    76 
    77 local
    78 
    79 val sig_int = 2;
    80 val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
    81 
    82 val _ = Signal.signal (sig_int, default_handler);
    83 val _ = PolyML.onEntry (fn () => (Signal.signal (sig_int, default_handler); ()));
    84 
    85 fun change_signal new_handler f x =
    86   let
    87     (*RACE wrt. other signals!*)
    88     val old_handler = Signal.signal (sig_int, new_handler);
    89     val result = Exn.capture (f old_handler) x;
    90     val _ = Signal.signal (sig_int, old_handler);
    91   in Exn.release result end;
    92 
    93 in
    94 
    95 fun interruptible f = change_signal default_handler (fn _ => f);
    96 
    97 fun uninterruptible f =
    98   change_signal Signal.SIG_IGN
    99     (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
   100 
   101 end;
   102 
   103 
   104 
   105 (** OS related **)
   106 
   107 (* current directory *)
   108 
   109 val cd = OS.FileSys.chDir;
   110 val pwd = OS.FileSys.getDir;
   111 
   112 
   113 (* getenv *)
   114 
   115 fun getenv var =
   116   (case OS.Process.getEnv var of
   117     NONE => ""
   118   | SOME txt => txt);
   119 
   120 
   121 
   122 (** Runtime system **)
   123 
   124 val exception_trace = PolyML.exception_trace;
   125 val timing = PolyML.timing;
   126 val profiling = PolyML.profiling;
   127 
   128 fun profile 0 f x = f x
   129   | profile n f x =
   130       let
   131         val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
   132         val res = Exn.capture f x;
   133         val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
   134       in Exn.release res end;
   135