author | wenzelm |
Thu, 04 Mar 2010 21:02:21 +0100 | |
changeset 35567 | 309e75c58af2 |
parent 32738 | 15bb09ca0378 |
permissions | -rw-r--r-- |
31312 | 1 |
(* Title: Pure/ML-Systems/compiler_polyml-5.0.ML |
2 |
||
31329 | 3 |
Runtime compilation for Poly/ML 5.0 and 5.1. |
31312 | 4 |
*) |
5 |
||
6 |
fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt = |
|
7 |
let |
|
32738 | 8 |
val in_buffer = Unsynchronized.ref (explode (tune_source txt)); |
9 |
val out_buffer = Unsynchronized.ref ([]: string list); |
|
31312 | 10 |
fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); |
11 |
||
32738 | 12 |
val current_line = Unsynchronized.ref line; |
31312 | 13 |
fun get () = |
14 |
(case ! in_buffer of |
|
15 |
[] => "" |
|
16 |
| c :: cs => (in_buffer := cs; if c = "\n" then current_line := ! current_line + 1 else (); c)); |
|
17 |
fun put s = out_buffer := s :: ! out_buffer; |
|
18 |
||
19 |
fun exec () = |
|
20 |
(case ! in_buffer of |
|
21 |
[] => () |
|
22 |
| _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ())); |
|
23 |
in |
|
31480
05937d6aafb5
reraise exceptions to preserve position information;
wenzelm
parents:
31329
diff
changeset
|
24 |
exec () handle exn => (error (output ()); reraise exn); |
31312 | 25 |
if verbose then print (output ()) else () |
26 |
end; |
|
27 |
||
28 |
fun use_file context verbose name = |
|
29 |
let |
|
30 |
val instream = TextIO.openIn name; |
|
31 |
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); |
|
32 |
in use_text context (1, name) verbose txt end; |