|
1 (* Title: Pure/ML-Systems/smlnj-0.93.ML |
|
2 ID: $Id$ |
|
3 Author: Carsten Clasohm, TU Muenchen |
|
4 Copyright 1996 TU Muenchen |
|
5 |
|
6 Compatibility file for Standard ML of New Jersey version 0.93. |
|
7 *) |
|
8 |
|
9 |
|
10 use"basis.ML"; |
|
11 |
|
12 |
|
13 (*** Poly/ML emulation ***) |
|
14 |
|
15 fun quit () = exit 0; |
|
16 |
|
17 (*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*) |
|
18 fun print_depth n = (System.Control.Print.printDepth := n div 2; |
|
19 System.Control.Print.printLength := n); |
|
20 |
|
21 (*Interface for toplevel pretty printers, see also Pure/install_pp.ML*) |
|
22 |
|
23 fun make_pp path pprint = |
|
24 let |
|
25 open System.PrettyPrint; |
|
26 |
|
27 fun pp pps obj = |
|
28 pprint obj |
|
29 (add_string pps, begin_block pps INCONSISTENT, |
|
30 fn wd => add_break pps (wd, 0), fn () => add_newline pps, |
|
31 fn () => end_block pps); |
|
32 in |
|
33 (path, pp) |
|
34 end; |
|
35 |
|
36 fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp; |
|
37 |
|
38 |
|
39 (*** New Jersey ML parameters ***) |
|
40 |
|
41 (* Suppresses Garbage Collection messages; default was 2 *) |
|
42 System.Control.Runtime.gcmessages := 0; |
|
43 |
|
44 |
|
45 (*** Timing functions ***) |
|
46 |
|
47 (*Print microseconds, suppressing trailing zeroes*) |
|
48 fun umakestring 0 = "" |
|
49 | umakestring n = chr(ord "0" + n div 100000) ^ |
|
50 umakestring(10 * (n mod 100000)); |
|
51 |
|
52 (*A conditional timing function: applies f to () and, if the flag is true, |
|
53 prints its runtime. *) |
|
54 fun cond_timeit flag f = |
|
55 if flag then |
|
56 let fun string_of_time (System.Timer.TIME {sec, usec}) = |
|
57 makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec) |
|
58 open System.Timer; |
|
59 val start = start_timer() |
|
60 val result = f(); |
|
61 val nongc = check_timer(start) |
|
62 and gc = check_timer_gc(start); |
|
63 val both = add_time(nongc, gc) |
|
64 in print("Non GC " ^ string_of_time nongc ^ |
|
65 " GC " ^ string_of_time gc ^ |
|
66 " both "^ string_of_time both ^ " secs\n"); |
|
67 result |
|
68 end |
|
69 else f(); |
|
70 |
|
71 |
|
72 (*** File handling ***) |
|
73 |
|
74 (*Get time of last modification; if file doesn't exist return an empty string*) |
|
75 local |
|
76 open System.Timer; |
|
77 open System.Unsafe.SysIO; |
|
78 in |
|
79 fun file_info "" = "" |
|
80 | file_info name = makestring (mtime (PATH name)) handle _ => ""; |
|
81 end; |
|
82 |
|
83 structure OS = |
|
84 struct |
|
85 structure FileSys = |
|
86 struct |
|
87 val chDir = System.Directory.cd |
|
88 val remove = System.Unsafe.SysIO.unlink (*Delete a file *) |
|
89 val getDir = System.Directory.getWD (*path of working directory*) |
|
90 end |
|
91 end; |
|
92 |
|
93 |
|
94 (*** ML command execution ***) |
|
95 |
|
96 fun use_string commands = |
|
97 System.Compile.use_stream (open_string (implode commands)); |
|
98 |
|
99 |
|
100 (*** System command execution ***) |
|
101 |
|
102 (*Execute an Unix command which doesn't take any input from stdin and |
|
103 sends its output to stdout. |
|
104 This could be done more easily by IO.execute, but that function |
|
105 seems to be buggy in SML/NJ 0.93.*) |
|
106 fun execute command = |
|
107 let val tmp_name = "isa_converted.tmp" |
|
108 val is = (System.system (command ^ " > " ^ tmp_name); |
|
109 open_in tmp_name); |
|
110 val result = input (is, 999999); |
|
111 in close_in is; |
|
112 OS.FileSys.remove tmp_name; |
|
113 result |
|
114 end; |
|
115 |
|
116 (*redefine to flush its output immediately -- temporary patch suggested |
|
117 by Kim Dam Petersen*) |
|
118 val output = fn(s, t) => (output(s, t); flush_out s); |
|
119 |
|
120 |
|
121 (* symbol input *) |
|
122 |
|
123 val needs_filtered_use = false; |