author | haftmann |
Mon, 08 Feb 2010 17:12:22 +0100 | |
changeset 35045 | a77d200e6503 |
parent 33538 | edf497b5b5d2 |
child 38470 | 484e483eb606 |
permissions | -rw-r--r-- |
31312 | 1 |
(* Title: Pure/ML-Systems/compiler_polyml-5.3.ML |
2 |
||
33538
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
32738
diff
changeset
|
3 |
Runtime compilation for Poly/ML 5.3.0. |
31312 | 4 |
*) |
5 |
||
6 |
local |
|
7 |
||
8 |
fun drop_newline s = |
|
9 |
if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) |
|
10 |
else s; |
|
11 |
||
12 |
in |
|
13 |
||
14 |
fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context) |
|
15 |
(start_line, name) verbose txt = |
|
16 |
let |
|
32738 | 17 |
val line = Unsynchronized.ref start_line; |
18 |
val in_buffer = Unsynchronized.ref (String.explode (tune_source txt)); |
|
19 |
val out_buffer = Unsynchronized.ref ([]: string list); |
|
31312 | 20 |
fun output () = drop_newline (implode (rev (! out_buffer))); |
21 |
||
22 |
fun get () = |
|
23 |
(case ! in_buffer of |
|
24 |
[] => NONE |
|
31471 | 25 |
| c :: cs => (in_buffer := cs; if c = #"\n" then line := ! line + 1 else (); SOME c)); |
31312 | 26 |
fun put s = out_buffer := s :: ! out_buffer; |
27 |
fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} = |
|
28 |
(put (if hard then "Error: " else "Warning: "); |
|
29 |
PolyML.prettyPrint (put, 76) msg1; |
|
30 |
(case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2); |
|
31 |
put ("At" ^ str_of_pos line name ^ "\n")); |
|
32 |
||
33 |
val parameters = |
|
34 |
[PolyML.Compiler.CPOutStream put, |
|
31471 | 35 |
PolyML.Compiler.CPNameSpace name_space, |
31312 | 36 |
PolyML.Compiler.CPErrorMessageProc put_message, |
31471 | 37 |
PolyML.Compiler.CPLineNo (fn () => ! line), |
38 |
PolyML.Compiler.CPFileName name, |
|
31312 | 39 |
PolyML.Compiler.CPPrintInAlphabeticalOrder false]; |
40 |
val _ = |
|
41 |
(while not (List.null (! in_buffer)) do |
|
42 |
PolyML.compiler (get, parameters) ()) |
|
43 |
handle exn => |
|
44 |
(put ("Exception- " ^ General.exnMessage exn ^ " raised"); |
|
31480
05937d6aafb5
reraise exceptions to preserve position information;
wenzelm
parents:
31471
diff
changeset
|
45 |
error (output ()); reraise exn); |
31312 | 46 |
in if verbose then print (output ()) else () end; |
47 |
||
48 |
fun use_file context verbose name = |
|
49 |
let |
|
50 |
val instream = TextIO.openIn name; |
|
51 |
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); |
|
52 |
in use_text context (1, name) verbose txt end; |
|
53 |
||
54 |
end; |
|
55 |