author | wenzelm |
Mon, 24 Mar 2008 18:35:48 +0100 | |
changeset 26382 | 16628f5c7e28 |
child 26385 | ae7564661e76 |
permissions | -rw-r--r-- |
26382
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/polyml_old_compiler4.ML |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
3 |
|
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
4 |
Runtime compilation -- for old version of PolyML.compiler (version 4.x). |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
5 |
*) |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
6 |
|
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
7 |
fun use_text (tune: string -> string) name (print, err) verbose txt = |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
8 |
let |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
9 |
val in_buffer = ref (explode (tune txt)); |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
10 |
val out_buffer = ref ([]: string list); |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
11 |
fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
12 |
|
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
13 |
fun get () = |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
14 |
(case ! in_buffer of |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
15 |
[] => "" |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
16 |
| c :: cs => (in_buffer := cs; c)); |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
17 |
fun put s = out_buffer := s :: ! out_buffer; |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
18 |
|
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
19 |
fun exec () = |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
20 |
(case ! in_buffer of |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
21 |
[] => () |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
22 |
| _ => (PolyML.compiler (get, put) (); exec ())); |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
23 |
in |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
24 |
exec () handle exn => |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
25 |
(err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn); |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
26 |
if verbose then print (output ()) else () |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
27 |
end; |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
28 |
|
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
29 |
fun use_file tune output verbose name = |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
30 |
let |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
31 |
val instream = TextIO.openIn name; |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
32 |
val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
33 |
in use_text tune name output verbose txt end; |
16628f5c7e28
Runtime compilation -- for old version of PolyML.compiler (version 4.x).
wenzelm
parents:
diff
changeset
|
34 |