src/Pure/ML-Systems/smlnj.ML
changeset 4403 1914f727f93f
child 4407 7d4e2832b791
equal deleted inserted replaced
4402:3b53dd8e9e23 4403:1914f727f93f
       
     1 (*  Title:      Pure/ML-Systems/smlnj.ML
       
     2     ID:         $Id$
       
     3     Author:     Carsten Clasohm and Markus Wenzel, TU Muenchen
       
     4 
       
     5 Compatibility file for Standard ML of New Jersey versions 109.27 to
       
     6 109.33, 110 or later.
       
     7 *)
       
     8 
       
     9 (** ML system related **)
       
    10 
       
    11 (* restore old-style character / string functions *)
       
    12 
       
    13 fun ord s = Char.ord (String.sub (s, 0));
       
    14 val chr = str o Char.chr;
       
    15 val explode = (map str) o String.explode;
       
    16 val implode = String.concat;
       
    17 
       
    18 
       
    19 (* New Jersey ML parameters *)
       
    20 
       
    21 val _ =
       
    22  (Compiler.Control.Print.printLength := 1000;
       
    23   Compiler.Control.Print.printDepth := 350;
       
    24   Compiler.Control.Print.stringDepth := 250;
       
    25   Compiler.Control.Print.signatures := 2);
       
    26 
       
    27 
       
    28 (* Poly/ML emulation *)
       
    29 
       
    30 fun quit () = exit 0;
       
    31 
       
    32 (*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
       
    33 fun print_depth n =
       
    34  (Compiler.Control.Print.printDepth := n div 2;
       
    35   Compiler.Control.Print.printLength := n);
       
    36 
       
    37 (*Poly/ML-like prompts*)
       
    38 Compiler.Control.primaryPrompt := "> ";
       
    39 Compiler.Control.secondaryPrompt := "# ";
       
    40 
       
    41 
       
    42 (** Compiler-independent timing functions **)
       
    43 
       
    44 (*Note start point for timing*)
       
    45 fun startTiming() = 
       
    46   let val CPUtimer = Timer.startCPUTimer();
       
    47       val time = Timer.checkCPUTimer(CPUtimer)
       
    48   in  (CPUtimer,time)  end;
       
    49 
       
    50 (*Finish timing and return string*)
       
    51 fun endTiming (CPUtimer, {gc,sys,usr}) =
       
    52   let open Time  (*...for Time.toString, Time.+ and Time.- *)
       
    53       val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
       
    54   in  "User " ^ toString (usr2-usr) ^
       
    55       "  GC " ^ toString (gc2-gc) ^
       
    56       "  All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^
       
    57       " secs"
       
    58       handle Time => ""
       
    59   end;
       
    60 
       
    61 
       
    62 (* toplevel pretty printing (see also Pure/install_pp.ML) *)
       
    63 
       
    64 fun make_pp path pprint =
       
    65   let
       
    66     open Compiler.PrettyPrint;
       
    67 
       
    68     fun pp pps obj =
       
    69       pprint obj
       
    70         (add_string pps, begin_block pps INCONSISTENT,
       
    71           fn wd => add_break pps (wd, 0), fn () => add_newline pps,
       
    72           fn () => end_block pps);
       
    73   in
       
    74     (path, pp)
       
    75   end;
       
    76 
       
    77 fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp;
       
    78 
       
    79 
       
    80 (* ML command execution *)
       
    81 
       
    82 val use_strings = Compiler.Interact.useStream o TextIO.openString o implode;
       
    83 
       
    84 
       
    85 
       
    86 (** OS related **)
       
    87 
       
    88 (* system command execution *)
       
    89 
       
    90 (*execute Unix command which doesn't take any input from stdin and
       
    91   sends its output to stdout; could be done more easily by Unix.execute,
       
    92   but that function doesn't use the PATH*)
       
    93 fun execute command =
       
    94   let
       
    95     val tmp_name = OS.FileSys.tmpName ();
       
    96     val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
       
    97     val result = TextIO.inputAll is;
       
    98   in
       
    99     TextIO.closeIn is;
       
   100     OS.FileSys.remove tmp_name;
       
   101     result
       
   102   end;
       
   103 
       
   104 
       
   105 (* file handling *)
       
   106 
       
   107 (*get time of last modification; if file doesn't exist return an empty string*)
       
   108 fun file_info "" = ""		(* FIXME !? *)
       
   109   | file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
       
   110 
       
   111 
       
   112 (* getenv *)
       
   113 
       
   114 fun getenv var =
       
   115   (case OS.Process.getEnv var of
       
   116     NONE => ""
       
   117   | SOME txt => txt);
       
   118 
       
   119 
       
   120 (* non-ASCII input (see also Thy/symbol_input.ML) *)
       
   121 
       
   122 val needs_filtered_use = false;