author | wenzelm |
Wed, 23 Dec 2015 23:09:13 +0100 | |
changeset 61925 | ab52f183f020 |
parent 60956 | src/Pure/ML-Systems/compiler_polyml.ML@10d463883dc2 |
child 62354 | fdd6989cc8a0 |
permissions | -rw-r--r-- |
61925 | 1 |
(* Title: Pure/RAW/compiler_polyml.ML |
31312 | 2 |
|
50910 | 3 |
Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML). |
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) |
|
60956 | 15 |
{line, file, verbose, debug} text = |
31312 | 16 |
let |
60955 | 17 |
val current_line = Unsynchronized.ref line; |
56435
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
50910
diff
changeset
|
18 |
val in_buffer = |
60956 | 19 |
Unsynchronized.ref (String.explode (tune_source (ml_positions line file text))); |
32738 | 20 |
val out_buffer = Unsynchronized.ref ([]: string list); |
31312 | 21 |
fun output () = drop_newline (implode (rev (! out_buffer))); |
22 |
||
23 |
fun get () = |
|
24 |
(case ! in_buffer of |
|
25 |
[] => NONE |
|
60955 | 26 |
| c :: cs => |
27 |
(in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); |
|
31312 | 28 |
fun put s = out_buffer := s :: ! out_buffer; |
60955 | 29 |
fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} = |
31312 | 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); |
|
60955 | 33 |
put ("At" ^ str_of_pos message_line file ^ "\n")); |
31312 | 34 |
|
35 |
val parameters = |
|
36 |
[PolyML.Compiler.CPOutStream put, |
|
31471 | 37 |
PolyML.Compiler.CPNameSpace name_space, |
31312 | 38 |
PolyML.Compiler.CPErrorMessageProc put_message, |
60955 | 39 |
PolyML.Compiler.CPLineNo (fn () => ! current_line), |
40 |
PolyML.Compiler.CPFileName file, |
|
60956 | 41 |
PolyML.Compiler.CPPrintInAlphabeticalOrder false] @ |
42 |
ML_Compiler_Parameters.debug debug; |
|
31312 | 43 |
val _ = |
44 |
(while not (List.null (! in_buffer)) do |
|
45 |
PolyML.compiler (get, parameters) ()) |
|
46 |
handle exn => |
|
39242
28d3809ff91f
primitive use_text: let interrupts pass unhindered;
wenzelm
parents:
38470
diff
changeset
|
47 |
if Exn.is_interrupt exn then reraise exn |
28d3809ff91f
primitive use_text: let interrupts pass unhindered;
wenzelm
parents:
38470
diff
changeset
|
48 |
else |
28d3809ff91f
primitive use_text: let interrupts pass unhindered;
wenzelm
parents:
38470
diff
changeset
|
49 |
(put ("Exception- " ^ General.exnMessage exn ^ " raised"); |
28d3809ff91f
primitive use_text: let interrupts pass unhindered;
wenzelm
parents:
38470
diff
changeset
|
50 |
error (output ()); reraise exn); |
31312 | 51 |
in if verbose then print (output ()) else () end; |
52 |
||
60956 | 53 |
fun use_file context {verbose, debug} file = |
31312 | 54 |
let |
60955 | 55 |
val instream = TextIO.openIn file; |
60956 | 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; |
|
31312 | 58 |
|
59 |
end; |