author | paulson |
Wed, 09 Oct 1996 13:32:33 +0200 | |
changeset 2073 | fb0655539d05 |
parent 1480 | 85ecd3439e01 |
child 2141 | c2aedd8169cd |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: Pure/POLY |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1991 University of Cambridge |
|
5 |
||
6 |
Compatibility file for Poly/ML (AHL release 1.88) |
|
7 |
*) |
|
8 |
||
9 |
open PolyML ExtendedIO; |
|
10 |
||
11 |
||
12 |
(*A conditional timing function: applies f to () and, if the flag is true, |
|
13 |
prints its runtime.*) |
|
14 |
||
15 |
fun cond_timeit flag f = |
|
16 |
if flag then |
|
17 |
let val before = System.processtime() |
|
18 |
val result = f() |
|
19 |
val both = real(System.processtime() - before) / 10.0 |
|
20 |
in output(std_out, "Process time (incl GC): "^ |
|
21 |
makestring both ^ " secs\n"); |
|
22 |
result |
|
23 |
end |
|
24 |
else f(); |
|
25 |
||
26 |
||
27 |
(*Save function: in Poly/ML, ignores filename and commits to present file*) |
|
28 |
||
29 |
fun xML filename banner = commit(); |
|
30 |
||
31 |
||
32 |
(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*) |
|
33 |
||
34 |
fun make_pp _ pprint (str, blk, brk, en) obj = |
|
19 | 35 |
pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0), |
36 |
fn () => brk (99999, 0), en); |
|
0 | 37 |
|
38 |
||
66 | 39 |
(*** File handling ***) |
0 | 40 |
|
100
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
41 |
local |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
42 |
|
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
43 |
(*These are functions from library.ML *) |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
44 |
fun take_suffix _ [] = ([], []) |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
45 |
| take_suffix pred (x :: xs) = |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
46 |
(case take_suffix pred xs of |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
47 |
([], sffx) => if pred x then ([], x :: sffx) |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
48 |
else ([x], sffx) |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
49 |
| (prfx, sffx) => (x :: prfx, sffx)); |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
50 |
|
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
51 |
fun apr (f,y) x = f(x,y); |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
52 |
|
396
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
53 |
fun seq (proc: 'a -> unit) : 'a list -> unit = |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
54 |
let fun seqf [] = () |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
55 |
| seqf (x :: xs) = (proc x; seqf xs) |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
56 |
in seqf end; |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
57 |
|
1437 | 58 |
fun radixpand num : int list = |
59 |
let fun radix (n, tail) = |
|
60 |
if n < 10 then n :: tail else radix (n div 10, (n mod 10) :: tail) |
|
61 |
in radix (num, []) end; |
|
62 |
||
63 |
fun radixstring num = |
|
64 |
let fun chrof n = chr (ord "0" + n); |
|
65 |
in implode (map chrof (radixpand num)) end; |
|
66 |
||
100
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
67 |
in |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
68 |
|
1480 | 69 |
(*Get time of last modification; if file doesn't exist return an empty string*) |
0 | 70 |
fun file_info "" = "" |
1480 | 71 |
| file_info name = radixstring (System.filedate name) handle _ => ""; |
66 | 72 |
|
73
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
66
diff
changeset
|
73 |
(*Delete a file *) |
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
66
diff
changeset
|
74 |
fun delete_file name = |
100
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
75 |
let val (is, os) = ExtendedIO.execute ("rm " ^ name) |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
76 |
in close_in is; |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
77 |
close_out os |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
78 |
end; |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
79 |
|
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
80 |
(*Get pathname of current working directory *) |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
81 |
fun pwd () = |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
82 |
let val (is, os) = ExtendedIO.execute ("pwd") |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
83 |
val (path, _) = take_suffix (apr(op=,"\n")) |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
84 |
(explode (ExtendedIO.input_line is)) (*remove newline *) |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
85 |
in close_in is; |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
86 |
close_out os; |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
87 |
implode path |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
88 |
end; |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
89 |
|
378
85ff48546a05
added use_string: string -> unit to execute ML commands passed in a string
clasohm
parents:
100
diff
changeset
|
90 |
|
85ff48546a05
added use_string: string -> unit to execute ML commands passed in a string
clasohm
parents:
100
diff
changeset
|
91 |
(*** ML command execution ***) |
85ff48546a05
added use_string: string -> unit to execute ML commands passed in a string
clasohm
parents:
100
diff
changeset
|
92 |
|
396
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
93 |
val use_string = |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
94 |
let fun exec command = |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
95 |
let val firstLine = ref true; |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
96 |
|
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
97 |
fun getLine () = |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
98 |
if !firstLine |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
99 |
then (firstLine := false; command) |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
100 |
else raise Io "use_string: buffer exhausted" |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
101 |
in PolyML.compiler (getLine, fn s => output (std_out, s)) () end |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
102 |
in seq exec end; |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
103 |
|
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
104 |
end; |
1289 | 105 |
|
106 |
||
107 |
(*** System command execution ***) |
|
108 |
||
109 |
(*Execute an Unix command which doesn't take any input from stdin and |
|
110 |
sends its output to stdout.*) |
|
111 |
fun execute command = |
|
112 |
let val (is, os) = ExtendedIO.execute command; |
|
113 |
val result = input (is, 999999); |
|
114 |
in close_out os; |
|
115 |
close_in is; |
|
116 |
result |
|
117 |
end; |