author | wenzelm |
Mon, 15 Jun 2015 13:29:57 +0200 | |
changeset 60483 | 9a566f4ac20a |
parent 56435 | 28b34e8e4a80 |
child 60955 | 65149ae760a0 |
permissions | -rw-r--r-- |
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
41717
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/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) |
|
15 |
(start_line, name) verbose txt = |
|
16 |
let |
|
32738 | 17 |
val line = Unsynchronized.ref start_line; |
56435
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
50910
diff
changeset
|
18 |
val in_buffer = |
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
50910
diff
changeset
|
19 |
Unsynchronized.ref (String.explode (tune_source (ml_positions start_line name txt))); |
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 |
|
31471 | 26 |
| c :: cs => (in_buffer := cs; if c = #"\n" then line := ! line + 1 else (); SOME c)); |
31312 | 27 |
fun put s = out_buffer := s :: ! out_buffer; |
28 |
fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} = |
|
29 |
(put (if hard then "Error: " else "Warning: "); |
|
30 |
PolyML.prettyPrint (put, 76) msg1; |
|
31 |
(case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2); |
|
32 |
put ("At" ^ str_of_pos line name ^ "\n")); |
|
33 |
||
34 |
val parameters = |
|
35 |
[PolyML.Compiler.CPOutStream put, |
|
31471 | 36 |
PolyML.Compiler.CPNameSpace name_space, |
31312 | 37 |
PolyML.Compiler.CPErrorMessageProc put_message, |
31471 | 38 |
PolyML.Compiler.CPLineNo (fn () => ! line), |
39 |
PolyML.Compiler.CPFileName name, |
|
31312 | 40 |
PolyML.Compiler.CPPrintInAlphabeticalOrder false]; |
41 |
val _ = |
|
42 |
(while not (List.null (! in_buffer)) do |
|
43 |
PolyML.compiler (get, parameters) ()) |
|
44 |
handle exn => |
|
39242
28d3809ff91f
primitive use_text: let interrupts pass unhindered;
wenzelm
parents:
38470
diff
changeset
|
45 |
if Exn.is_interrupt exn then reraise exn |
28d3809ff91f
primitive use_text: let interrupts pass unhindered;
wenzelm
parents:
38470
diff
changeset
|
46 |
else |
28d3809ff91f
primitive use_text: let interrupts pass unhindered;
wenzelm
parents:
38470
diff
changeset
|
47 |
(put ("Exception- " ^ General.exnMessage exn ^ " raised"); |
28d3809ff91f
primitive use_text: let interrupts pass unhindered;
wenzelm
parents:
38470
diff
changeset
|
48 |
error (output ()); reraise exn); |
31312 | 49 |
in if verbose then print (output ()) else () end; |
50 |
||
51 |
fun use_file context verbose name = |
|
52 |
let |
|
53 |
val instream = TextIO.openIn name; |
|
54 |
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); |
|
55 |
in use_text context (1, name) verbose txt end; |
|
56 |
||
57 |
end; |
|
58 |