author | wenzelm |
Mon, 23 Mar 2009 21:40:11 +0100 | |
changeset 30673 | 60568c168040 |
parent 30638 | 15cc4ad0e6e9 |
child 30676 | edca392a2abb |
permissions | -rw-r--r-- |
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/polyml.ML |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
2 |
|
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
3 |
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1. |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
4 |
*) |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
5 |
|
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
6 |
open Thread; |
30673 | 7 |
|
8 |
structure ML_Name_Space = |
|
9 |
struct |
|
10 |
open PolyML.NameSpace; |
|
11 |
type T = PolyML.NameSpace.nameSpace; |
|
12 |
val global = PolyML.globalNameSpace; |
|
13 |
end; |
|
14 |
||
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
15 |
use "ML-Systems/polyml_common.ML"; |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
16 |
use "ML-Systems/multithreading_polyml.ML"; |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
17 |
|
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
18 |
val pointer_eq = PolyML.pointerEq; |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
19 |
|
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
20 |
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
21 |
|
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
22 |
|
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
23 |
(* runtime compilation *) |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
24 |
|
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
25 |
local |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
26 |
|
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
27 |
fun drop_newline s = |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
28 |
if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
29 |
else s; |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
30 |
|
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
31 |
in |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
32 |
|
30673 | 33 |
fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context) |
34 |
(start_line, name) verbose txt = |
|
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
35 |
let |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
36 |
val current_line = ref start_line; |
30673 | 37 |
val in_buffer = ref (String.explode (tune_source txt)); |
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
38 |
val out_buffer = ref ([]: string list); |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
39 |
fun output () = drop_newline (implode (rev (! out_buffer))); |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
40 |
|
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
41 |
fun get () = |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
42 |
(case ! in_buffer of |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
43 |
[] => NONE |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
44 |
| c :: cs => |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
45 |
(in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
46 |
fun put s = out_buffer := s :: ! out_buffer; |
30673 | 47 |
fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} = |
30205 | 48 |
(put (if hard then "Error: " else "Warning: "); |
30673 | 49 |
PolyML.prettyPrint (put, 76) msg1; |
50 |
(case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2); |
|
51 |
put ("At" ^ str_of_pos line name ^ "\n")); |
|
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
52 |
|
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
53 |
val parameters = |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
54 |
[PolyML.Compiler.CPOutStream put, |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
55 |
PolyML.Compiler.CPLineNo (fn () => ! current_line), |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
56 |
PolyML.Compiler.CPErrorMessageProc put_message, |
30205 | 57 |
PolyML.Compiler.CPNameSpace name_space, |
58 |
PolyML.Compiler.CPPrintInAlphabeticalOrder false]; |
|
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
59 |
val _ = |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
60 |
(while not (List.null (! in_buffer)) do |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
61 |
PolyML.compiler (get, parameters) ()) |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
62 |
handle exn => |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
63 |
(put ("Exception- " ^ General.exnMessage exn ^ " raised"); |
30673 | 64 |
error (output ()); raise exn); |
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
65 |
in if verbose then print (output ()) else () end; |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
66 |
|
30673 | 67 |
fun use_file context verbose name = |
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
68 |
let |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
69 |
val instream = TextIO.openIn name; |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
70 |
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); |
30673 | 71 |
in use_text context (1, name) verbose txt end; |
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
72 |
|
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
73 |
end; |
30626 | 74 |
|
75 |
||
76 |
(* toplevel pretty printing *) |
|
77 |
||
30638 | 78 |
fun pretty_ml (PrettyBlock (ind, _, _, prts)) = ML_Pretty.Block (("", ""), map pretty_ml prts, ind) |
79 |
| pretty_ml (PrettyString s) = ML_Pretty.String (s, size s) |
|
80 |
| pretty_ml (PrettyBreak (wd, _)) = ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2)); |
|
81 |
||
30626 | 82 |
fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts) |
83 |
| ml_pretty (ML_Pretty.String (s, _)) = PrettyString s |
|
84 |
| ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0) |
|
85 |
| ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0); |
|
86 |
||
30673 | 87 |
fun toplevel_pp context (_: string list) pp = |
88 |
use_text context (1, "pp") false |
|
30626 | 89 |
("addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))"); |
90 |