|
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 = |
|
35 pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0), en); |
|
36 |
|
37 |
|
38 (*** File information ***) |
|
39 |
|
40 (*Get time of last modification.*) |
|
41 fun file_info "" = "" |
|
42 | file_info name = |
|
43 let val (is, os) = ExtendedIO.execute ("ls -l " ^ name) |
|
44 val result = ExtendedIO.input_line is; |
|
45 val dummy = close_in is; |
|
46 val dummy = close_out os; |
|
47 in result end; |
|
48 |