1 (* Title: Pure/ML-Systems/compiler_polyml.ML |
|
2 |
|
3 Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML). |
|
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 {line, file, verbose, debug} text = |
|
16 let |
|
17 val current_line = Unsynchronized.ref line; |
|
18 val in_buffer = |
|
19 Unsynchronized.ref (String.explode (tune_source (ml_positions line file text))); |
|
20 val out_buffer = Unsynchronized.ref ([]: string list); |
|
21 fun output () = drop_newline (implode (rev (! out_buffer))); |
|
22 |
|
23 fun get () = |
|
24 (case ! in_buffer of |
|
25 [] => NONE |
|
26 | c :: cs => |
|
27 (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); |
|
28 fun put s = out_buffer := s :: ! out_buffer; |
|
29 fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} = |
|
30 (put (if hard then "Error: " else "Warning: "); |
|
31 PolyML.prettyPrint (put, 76) msg1; |
|
32 (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2); |
|
33 put ("At" ^ str_of_pos message_line file ^ "\n")); |
|
34 |
|
35 val parameters = |
|
36 [PolyML.Compiler.CPOutStream put, |
|
37 PolyML.Compiler.CPNameSpace name_space, |
|
38 PolyML.Compiler.CPErrorMessageProc put_message, |
|
39 PolyML.Compiler.CPLineNo (fn () => ! current_line), |
|
40 PolyML.Compiler.CPFileName file, |
|
41 PolyML.Compiler.CPPrintInAlphabeticalOrder false] @ |
|
42 ML_Compiler_Parameters.debug debug; |
|
43 val _ = |
|
44 (while not (List.null (! in_buffer)) do |
|
45 PolyML.compiler (get, parameters) ()) |
|
46 handle exn => |
|
47 if Exn.is_interrupt exn then reraise exn |
|
48 else |
|
49 (put ("Exception- " ^ General.exnMessage exn ^ " raised"); |
|
50 error (output ()); reraise exn); |
|
51 in if verbose then print (output ()) else () end; |
|
52 |
|
53 fun use_file context {verbose, debug} file = |
|
54 let |
|
55 val instream = TextIO.openIn file; |
|
56 val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); |
|
57 in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end; |
|
58 |
|
59 end; |
|