equal
deleted
inserted
replaced
47 fn () => brk (99999, 0), en); |
47 fn () => brk (99999, 0), en); |
48 |
48 |
49 |
49 |
50 (* ML command execution -- 'eval' *) |
50 (* ML command execution -- 'eval' *) |
51 |
51 |
52 fun use_text verbose txt = |
52 fun use_text print verbose txt = |
53 let |
53 let |
54 val in_buffer = ref (explode txt); |
54 val in_buffer = ref (explode txt); |
55 val out_buffer = ref ([]: string list); |
55 val out_buffer = ref ([]: string list); |
56 |
56 |
57 fun get () = |
57 fun get () = |
99 (*execute Unix command which doesn't take any input from stdin and |
99 (*execute Unix command which doesn't take any input from stdin and |
100 sends its output to stdout*) |
100 sends its output to stdout*) |
101 fun execute command = |
101 fun execute command = |
102 let |
102 let |
103 val (is, os) = ExtendedIO.execute command; |
103 val (is, os) = ExtendedIO.execute command; |
|
104 val _ = close_out os; |
104 val result = input (is, 999999); |
105 val result = input (is, 999999); |
105 in |
106 in close_in is; result end; |
106 close_out os; |
107 |
107 close_in is; |
108 fun system cmd = (print (execute cmd); 0); (* FIXME rc not available *) |
108 result |
|
109 end; |
|
110 |
109 |
111 |
110 |
112 (* file handling *) |
111 (* file handling *) |
113 |
112 |
114 (*get time of last modification*) |
113 (*get time of last modification*) |