1 (* Title: Pure/ML-Systems/smlnj-1.07.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 1.07. |
|
7 *) |
|
8 |
|
9 use "basis.ML"; |
|
10 |
|
11 |
|
12 (*** Poly/ML emulation ***) |
|
13 |
|
14 fun quit () = exit 0; |
|
15 |
|
16 (*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*) |
|
17 fun print_depth n = (Compiler.Control.Print.printDepth := n div 2; |
|
18 Compiler.Control.Print.printLength := n); |
|
19 |
|
20 (*Interface for toplevel pretty printers, see also Pure/install_pp.ML*) |
|
21 |
|
22 fun make_pp path pprint = |
|
23 let |
|
24 open Compiler.PrettyPrint; |
|
25 |
|
26 fun pp pps obj = |
|
27 pprint obj |
|
28 (add_string pps, begin_block pps INCONSISTENT, |
|
29 fn wd => add_break pps (wd, 0), fn () => add_newline pps, |
|
30 fn () => end_block pps); |
|
31 in |
|
32 (path, pp) |
|
33 end; |
|
34 |
|
35 fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp; |
|
36 |
|
37 |
|
38 (*** New Jersey ML parameters ***) |
|
39 |
|
40 (* Suppresses Garbage Collection messages; doesn't work yet *) |
|
41 (*System.Runtime.gc 0;*) |
|
42 |
|
43 val _ = (Compiler.Control.Print.printLength := 1000; |
|
44 Compiler.Control.Print.printDepth := 350; |
|
45 Compiler.Control.Print.stringDepth := 250; |
|
46 Compiler.Control.Print.signatures := 2); |
|
47 |
|
48 |
|
49 (*** Character/string functions which are compatible with 0.93 and Poly/ML ***) |
|
50 |
|
51 fun ord s = Char.ord (String.sub(s,0)); |
|
52 val chr = str o Char.chr; |
|
53 val explode = (map str) o String.explode; |
|
54 val implode = String.concat; |
|
55 |
|
56 |
|
57 (*** Timing functions ***) |
|
58 |
|
59 (*Print microseconds, suppressing trailing zeroes*) |
|
60 fun umakestring 0 = "" |
|
61 | umakestring n = chr(ord "0" + n div 100000) ^ |
|
62 umakestring(10 * (n mod 100000)); |
|
63 |
|
64 (*A conditional timing function: applies f to () and, if the flag is true, |
|
65 prints its runtime. *) |
|
66 fun cond_timeit flag f = |
|
67 if flag then |
|
68 let fun string_of_time (System.Timer.TIME {sec, usec}) = |
|
69 makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec) |
|
70 open System.Timer; |
|
71 val start = start_timer() |
|
72 val result = f(); |
|
73 val nongc = check_timer(start) |
|
74 and gc = check_timer_gc(start); |
|
75 val both = add_time(nongc, gc) |
|
76 in print("Non GC " ^ string_of_time nongc ^ |
|
77 " GC " ^ string_of_time gc ^ |
|
78 " both "^ string_of_time both ^ " secs\n"); |
|
79 result |
|
80 end |
|
81 else f(); |
|
82 |
|
83 |
|
84 (*** File handling ***) |
|
85 |
|
86 (*Get time of last modification; if file doesn't exist return an empty string*) |
|
87 local |
|
88 open System.Timer; |
|
89 open System.Unsafe.SysIO; |
|
90 in |
|
91 fun file_info "" = "" |
|
92 | file_info name = makestring (mtime (PATH name)) handle _ => ""; |
|
93 end; |
|
94 |
|
95 structure OS = |
|
96 struct |
|
97 structure FileSys = |
|
98 struct |
|
99 val chDir = System.Directory.cd |
|
100 val remove = System.Unsafe.SysIO.unlink (*Delete a file *) |
|
101 val getDir = System.Directory.getWD (*path of working directory*) |
|
102 end |
|
103 end; |
|
104 |
|
105 |
|
106 |
|
107 (*** ML command execution ***) |
|
108 |
|
109 |
|
110 (*For version 109.21 and later: |
|
111 val use_string = Compiler.Interact.useStream o TextIO.openString o implode; |
|
112 *) |
|
113 |
|
114 (*For versions prior to 109.21:*) |
|
115 fun use_string commands = |
|
116 Compiler.Interact.use_stream (open_string (implode commands)); |
|
117 |
|
118 |
|
119 (*** System command execution ***) |
|
120 |
|
121 (*Execute an Unix command which doesn't take any input from stdin and |
|
122 sends its output to stdout. |
|
123 This could be done more easily by Unix.execute, but that function |
|
124 doesn't use the PATH.*) |
|
125 fun execute command = |
|
126 let val tmp_name = "isa_converted.tmp" |
|
127 val is = (System.Unix.system (command ^ " > " ^ tmp_name); |
|
128 open_in tmp_name); |
|
129 val result = input (is, 999999); |
|
130 in close_in is; |
|
131 OS.FileSys.remove tmp_name; |
|
132 result |
|
133 end; |
|
134 |
|
135 |
|
136 (* symbol input *) |
|
137 |
|
138 val needs_filtered_use = false; |
|