1 (* Title: Pure/RAW/ml_compiler0.ML |
|
2 |
|
3 Runtime compilation and evaluation (bootstrap version of |
|
4 Pure/ML/ml_compiler.ML). |
|
5 *) |
|
6 |
|
7 signature ML_COMPILER0 = |
|
8 sig |
|
9 type context = |
|
10 {name_space: ML_Name_Space.T, |
|
11 here: int -> string -> string, |
|
12 print: string -> unit, |
|
13 error: string -> unit} |
|
14 val use_text: context -> {debug: bool, file: string, line: int, verbose: bool} -> string -> unit |
|
15 val use_file: context -> {debug: bool, verbose: bool} -> string -> unit |
|
16 val debug_option: bool option -> bool |
|
17 val use_operations: (bool option -> string -> unit) -> |
|
18 {use: string -> unit, use_debug: string -> unit, use_no_debug: string -> unit} |
|
19 end; |
|
20 |
|
21 structure ML_Compiler0: ML_COMPILER0 = |
|
22 struct |
|
23 |
|
24 type context = |
|
25 {name_space: ML_Name_Space.T, |
|
26 here: int -> string -> string, |
|
27 print: string -> unit, |
|
28 error: string -> unit}; |
|
29 |
|
30 fun drop_newline s = |
|
31 if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) |
|
32 else s; |
|
33 |
|
34 fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text = |
|
35 let |
|
36 val _ = Secure.deny_ml (); |
|
37 |
|
38 val current_line = Unsynchronized.ref line; |
|
39 val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text)); |
|
40 val out_buffer = Unsynchronized.ref ([]: string list); |
|
41 fun output () = drop_newline (implode (rev (! out_buffer))); |
|
42 |
|
43 fun get () = |
|
44 (case ! in_buffer of |
|
45 [] => NONE |
|
46 | c :: cs => |
|
47 (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); |
|
48 fun put s = out_buffer := s :: ! out_buffer; |
|
49 fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} = |
|
50 (put (if hard then "Error: " else "Warning: "); |
|
51 PolyML.prettyPrint (put, 76) msg1; |
|
52 (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2); |
|
53 put ("At" ^ here (FixedInt.toInt message_line) file ^ "\n")); |
|
54 |
|
55 val parameters = |
|
56 [PolyML.Compiler.CPOutStream put, |
|
57 PolyML.Compiler.CPNameSpace name_space, |
|
58 PolyML.Compiler.CPErrorMessageProc put_message, |
|
59 PolyML.Compiler.CPLineNo (fn () => ! current_line), |
|
60 PolyML.Compiler.CPFileName file, |
|
61 PolyML.Compiler.CPPrintInAlphabeticalOrder false] @ |
|
62 ML_Compiler_Parameters.debug debug; |
|
63 val _ = |
|
64 (while not (List.null (! in_buffer)) do |
|
65 PolyML.compiler (get, parameters) ()) |
|
66 handle exn => |
|
67 if Exn.is_interrupt exn then reraise exn |
|
68 else |
|
69 (put ("Exception- " ^ General.exnMessage exn ^ " raised"); |
|
70 error (output ()); reraise exn); |
|
71 in if verbose then print (output ()) else () end; |
|
72 |
|
73 fun use_file context {verbose, debug} file = |
|
74 let |
|
75 val instream = TextIO.openIn file; |
|
76 val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); |
|
77 in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end; |
|
78 |
|
79 |
|
80 fun debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true" |
|
81 | debug_option (SOME debug) = debug; |
|
82 |
|
83 fun use_operations (use_ : bool option -> string -> unit) = |
|
84 {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)}; |
|
85 |
|
86 end; |
|
87 |
|
88 val {use, use_debug, use_no_debug} = |
|
89 let |
|
90 val context: ML_Compiler0.context = |
|
91 {name_space = ML_Name_Space.global, |
|
92 here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")", |
|
93 print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut), |
|
94 error = fn s => error s}; |
|
95 in |
|
96 ML_Compiler0.use_operations (fn opt_debug => fn file => |
|
97 ML_Compiler0.use_file context |
|
98 {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file |
|
99 handle ERROR msg => (#print context msg; raise error "ML error")) |
|
100 end; |
|