1 (* Title: Pure/ML-Systems/polyml.ML |
|
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 (versions 2.x and 3.x). |
|
7 *) |
|
8 |
|
9 open PolyML ExtendedIO; |
|
10 |
|
11 (*needs the Basis Library emulation*) |
|
12 use "basis.ML"; |
|
13 |
|
14 |
|
15 structure String = |
|
16 struct |
|
17 fun substring (s,i,j) = StringBuiltIns.substring (s, i+1, j) |
|
18 handle Substring => raise Subscript |
|
19 fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1)) |
|
20 handle Subscript => false |
|
21 fun str (s : string) = s; |
|
22 fun translate f s = implode (map f (explode s)); |
|
23 end; |
|
24 |
|
25 |
|
26 (** ML system related **) |
|
27 |
|
28 (** Compiler-independent timing functions **) |
|
29 |
|
30 (*Note start point for timing*) |
|
31 fun startTiming() = System.processtime (); |
|
32 |
|
33 (*Finish timing and return string*) |
|
34 fun endTiming before = |
|
35 "User + GC: " ^ |
|
36 makestring (real (System.processtime () - before) / 10.0) ^ |
|
37 " secs"; |
|
38 |
|
39 |
|
40 (* prompts *) |
|
41 |
|
42 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); |
|
43 |
|
44 |
|
45 (* toplevel pretty printing (see also Pure/install_pp.ML) *) |
|
46 |
|
47 fun make_pp _ pprint (str, blk, brk, en) obj = |
|
48 pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0), |
|
49 fn () => brk (99999, 0), en); |
|
50 |
|
51 |
|
52 (* ML command execution -- 'eval' *) |
|
53 |
|
54 local |
|
55 |
|
56 fun drop_last [] = [] |
|
57 | drop_last [x] = [] |
|
58 | drop_last (x :: xs) = x :: drop_last xs; |
|
59 |
|
60 val drop_last_char = implode o drop_last o explode; |
|
61 |
|
62 in |
|
63 |
|
64 fun use_text (print, err) verbose txt = |
|
65 let |
|
66 val in_buffer = ref (explode txt); |
|
67 val out_buffer = ref ([]: string list); |
|
68 fun output () = drop_last_char (implode (rev (! out_buffer))); |
|
69 |
|
70 fun get () = |
|
71 (case ! in_buffer of |
|
72 [] => "" |
|
73 | c :: cs => (in_buffer := cs; c)); |
|
74 fun put s = out_buffer := s :: ! out_buffer; |
|
75 |
|
76 fun exec () = |
|
77 (case ! in_buffer of |
|
78 [] => () |
|
79 | _ => (PolyML.compiler (get, put) (); exec ())); |
|
80 in |
|
81 exec () handle exn => (err (output ()); raise exn); |
|
82 if verbose then print (output ()) else () |
|
83 end; |
|
84 |
|
85 |
|
86 |
|
87 (** interrupts **) (*Note: may get into race conditions*) |
|
88 |
|
89 fun ignore_interrupt f x = f x; |
|
90 fun raise_interrupt f x = f x; |
|
91 |
|
92 |
|
93 |
|
94 (** OS related **) |
|
95 |
|
96 (* system command execution *) |
|
97 |
|
98 (*execute Unix command which doesn't take any input from stdin and |
|
99 sends its output to stdout*) |
|
100 fun execute command = |
|
101 let |
|
102 val (is, os) = ExtendedIO.execute command; |
|
103 val _ = close_out os; |
|
104 val result = input (is, 999999); |
|
105 in close_in is; result end; |
|
106 |
|
107 fun system cmd = (print (execute cmd); 0); (* FIXME rc not available *) |
|
108 |
|
109 |
|
110 (* file handling *) |
|
111 |
|
112 (*get time of last modification*) |
|
113 fun file_info name = Int.toString (System.filedate name) handle _ => ""; |
|
114 |
|
115 structure OS = |
|
116 struct |
|
117 structure FileSys = |
|
118 struct |
|
119 val chDir = PolyML.cd; |
|
120 fun remove name = (execute ("rm " ^ name); ()); |
|
121 fun getDir () = drop_last_char (execute "pwd"); |
|
122 end; |
|
123 end; |
|
124 |
|
125 |
|
126 (* getenv *) |
|
127 |
|
128 fun getenv var = drop_last_char |
|
129 (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'")); |
|
130 |
|
131 |
|
132 end; |
|