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