author | wenzelm |
Mon, 29 Nov 1993 13:54:59 +0100 | |
changeset 169 | 1b2765146aab |
parent 100 | e95b98536b3d |
child 220 | e50ea2471e06 |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: Pure/NJ |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
Compatibility file for Standard ML of New Jersey. |
|
7 |
*) |
|
8 |
||
9 |
(*** Poly/ML emulation ***) |
|
10 |
||
11 |
(*To exit the system -- an alternative to ^D *) |
|
12 |
fun quit () = System.Unsafe.CInterface.exit 0; |
|
13 |
||
14 |
(*To change the current directory*) |
|
15 |
val cd = System.Directory.cd; |
|
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 |
||
22 |
(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*) |
|
23 |
||
24 |
fun make_pp path pprint = |
|
25 |
let |
|
26 |
open System.PrettyPrint; |
|
27 |
||
28 |
fun pp pps obj = |
|
29 |
pprint obj |
|
30 |
(add_string pps, begin_block pps INCONSISTENT, |
|
19 | 31 |
fn wd => add_break pps (wd, 0), fn () => add_newline pps, |
32 |
fn () => end_block pps); |
|
0 | 33 |
in |
34 |
(path, pp) |
|
35 |
end; |
|
36 |
||
37 |
fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp; |
|
38 |
||
39 |
||
40 |
(*** New Jersey ML parameters ***) |
|
41 |
||
42 |
(* Suppresses Garbage Collection messages; default was 2 *) |
|
43 |
System.Control.Runtime.gcmessages := 0; |
|
44 |
||
45 |
(*redefine to flush its output immediately -- temporary patch suggested |
|
46 |
by Kim Dam Petersen*) |
|
47 |
val output = fn(s, t) => (output(s, t); flush_out s); |
|
48 |
||
49 |
(*Dummy version of the Poly/ML function*) |
|
50 |
fun commit() = (); |
|
51 |
||
52 |
(*For use in Makefiles -- saves space*) |
|
53 |
fun xML filename banner = (exportML filename; print(banner^"\n")); |
|
54 |
||
55 |
(*** Timing functions ***) |
|
56 |
||
57 |
(*Print microseconds, suppressing trailing zeroes*) |
|
58 |
fun umakestring 0 = "" |
|
59 |
| umakestring n = chr(ord"0" + n div 100000) ^ |
|
60 |
umakestring(10 * (n mod 100000)); |
|
61 |
||
62 |
(*A conditional timing function: applies f to () and, if the flag is true, |
|
63 |
prints its runtime. *) |
|
64 |
fun cond_timeit flag f = |
|
65 |
if flag then |
|
66 |
let fun string_of_time (System.Timer.TIME {sec, usec}) = |
|
67 |
makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec) |
|
68 |
open System.Timer; |
|
69 |
val start = start_timer() |
|
70 |
val result = f(); |
|
71 |
val nongc = check_timer(start) |
|
72 |
and gc = check_timer_gc(start); |
|
73 |
val both = add_time(nongc, gc) |
|
74 |
in print("Non GC " ^ string_of_time nongc ^ |
|
75 |
" GC " ^ string_of_time gc ^ |
|
76 |
" both "^ string_of_time both ^ " secs\n"); |
|
77 |
result |
|
78 |
end |
|
79 |
else f(); |
|
80 |
||
81 |
||
66 | 82 |
(*** File handling ***) |
0 | 83 |
|
84 |
(*Get time of last modification.*) |
|
85 |
local |
|
86 |
open System.Timer; |
|
87 |
open System.Unsafe.SysIO; |
|
88 |
in |
|
89 |
fun file_info "" = "" |
|
90 |
| file_info name = makestring (mtime (PATH name)); |
|
91 |
end; |
|
92 |
||
73
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
66
diff
changeset
|
93 |
fun delete_file name = |
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
66
diff
changeset
|
94 |
let val _ = System.system ("rm " ^ name) |
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
66
diff
changeset
|
95 |
in () end; |
66 | 96 |
|
100
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
97 |
(*Get pathname of current working directory *) |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
98 |
fun pwd () = System.Directory.getWD (); |