author | wenzelm |
Thu, 16 Jul 2015 14:40:23 +0200 | |
changeset 60731 | 4ac4b314d93c |
parent 60729 | f5989a2c1f67 |
child 60745 | d86b4cd0f1ec |
permissions | -rw-r--r-- |
33538
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
32778
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/polyml.ML |
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
2 |
Author: Makarius |
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
3 |
|
50910 | 4 |
Compatibility wrapper for Poly/ML. |
29714
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 |
|
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
7 |
(* ML name space *) |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
8 |
|
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
9 |
structure ML_Name_Space = |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
10 |
struct |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
11 |
open PolyML.NameSpace; |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
12 |
type T = PolyML.NameSpace.nameSpace; |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
13 |
val global = PolyML.globalNameSpace; |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
14 |
val initial_val = |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
15 |
List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit") |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
16 |
(#allVal global ()); |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
17 |
val initial_type = #allType global (); |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
18 |
val initial_fixity = #allFix global (); |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
19 |
val initial_structure = #allStruct global (); |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
20 |
val initial_signature = #allSig global (); |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
21 |
val initial_functor = #allFunct global (); |
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59055
diff
changeset
|
22 |
val forget_global_structure = PolyML.Compiler.forgetStructure; |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
23 |
end; |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
24 |
|
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
54723
diff
changeset
|
25 |
|
54717 | 26 |
(* ML system operations *) |
27 |
||
28 |
use "ML-Systems/ml_system.ML"; |
|
29 |
||
30 |
if ML_System.name = "polyml-5.3.0" |
|
31 |
then use "ML-Systems/share_common_data_polyml-5.3.0.ML" |
|
32 |
else (); |
|
33 |
||
34 |
structure ML_System = |
|
35 |
struct |
|
36 |
||
37 |
open ML_System; |
|
38 |
||
39 |
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; |
|
40 |
val save_state = PolyML.SaveState.saveState; |
|
41 |
||
42 |
end; |
|
43 |
||
44 |
||
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
45 |
(* exceptions *) |
30673 | 46 |
|
31427
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset
|
47 |
fun reraise exn = |
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset
|
48 |
(case PolyML.exceptionLocation exn of |
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset
|
49 |
NONE => raise exn |
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset
|
50 |
| SOME location => PolyML.raiseWithLocation (exn, location)); |
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset
|
51 |
|
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
52 |
exception Interrupt = SML90.Interrupt; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
53 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
54 |
use "General/exn.ML"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
55 |
|
59470 | 56 |
fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace; |
57 |
||
58 |
if ML_System.name = "polyml-5.5.1" |
|
59 |
orelse ML_System.name = "polyml-5.5.2" |
|
60 |
orelse ML_System.name = "polyml-5.5.3" |
|
61 |
then use "ML-Systems/exn_trace_polyml-5.5.1.ML" |
|
62 |
else (); |
|
63 |
||
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
64 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
65 |
(* multithreading *) |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
66 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
67 |
val seconds = Time.fromReal; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
68 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
69 |
if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ()) |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
70 |
then () |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
71 |
else use "ML-Systems/single_assignment_polyml.ML"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
72 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
73 |
open Thread; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
74 |
use "ML-Systems/multithreading.ML"; |
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
75 |
use "ML-Systems/multithreading_polyml.ML"; |
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
76 |
|
59468
fe6651760643
explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
wenzelm
parents:
59127
diff
changeset
|
77 |
if ML_System.name = "polyml-5.5.3" |
fe6651760643
explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
wenzelm
parents:
59127
diff
changeset
|
78 |
then use "ML-Systems/maximum_ml_stack_polyml-5.5.3.ML" |
fe6651760643
explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
wenzelm
parents:
59127
diff
changeset
|
79 |
else use "ML-Systems/maximum_ml_stack_dummy.ML"; |
fe6651760643
explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
wenzelm
parents:
59127
diff
changeset
|
80 |
|
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38470
diff
changeset
|
81 |
use "ML-Systems/unsynchronized.ML"; |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38470
diff
changeset
|
82 |
val _ = PolyML.Compiler.forgetValue "ref"; |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38470
diff
changeset
|
83 |
val _ = PolyML.Compiler.forgetType "ref"; |
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
84 |
|
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
85 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
86 |
(* pervasive environment *) |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
87 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
88 |
val _ = PolyML.Compiler.forgetValue "isSome"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
89 |
val _ = PolyML.Compiler.forgetValue "getOpt"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
90 |
val _ = PolyML.Compiler.forgetValue "valOf"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
91 |
val _ = PolyML.Compiler.forgetValue "foldl"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
92 |
val _ = PolyML.Compiler.forgetValue "foldr"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
93 |
val _ = PolyML.Compiler.forgetValue "print"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
94 |
val _ = PolyML.Compiler.forgetValue "explode"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
95 |
val _ = PolyML.Compiler.forgetValue "concat"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
96 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
97 |
val ord = SML90.ord; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
98 |
val chr = SML90.chr; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
99 |
val raw_explode = SML90.explode; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
100 |
val implode = SML90.implode; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
101 |
|
54342
fbcaa9f08879
avoid non-portable int constant -- make SML/NJ happy;
wenzelm
parents:
53709
diff
changeset
|
102 |
val io_buffer_size = 4096; |
fbcaa9f08879
avoid non-portable int constant -- make SML/NJ happy;
wenzelm
parents:
53709
diff
changeset
|
103 |
|
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
104 |
fun quit () = exit 0; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
105 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
106 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
107 |
(* ML runtime system *) |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
108 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
109 |
val timing = PolyML.timing; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
110 |
val profiling = PolyML.profiling; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
111 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
112 |
fun profile 0 f x = f x |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
113 |
| profile n f x = |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
114 |
let |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
115 |
val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
116 |
val res = Exn.capture f x; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
117 |
val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
118 |
in Exn.release res end; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
119 |
|
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
120 |
val pointer_eq = PolyML.pointerEq; |
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset
|
121 |
|
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
122 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
123 |
(* ML compiler *) |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
124 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
125 |
use "ML-Systems/use_context.ML"; |
56435
28b34e8e4a80
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;
wenzelm
parents:
56303
diff
changeset
|
126 |
use "ML-Systems/ml_positions.ML"; |
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
127 |
use "ML-Systems/compiler_polyml.ML"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
128 |
|
32778 | 129 |
PolyML.Compiler.reportUnreferencedIds := true; |
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
130 |
PolyML.Compiler.printInAlphabeticalOrder := false; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
131 |
PolyML.Compiler.maxInlineSize := 80; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
132 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
133 |
fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); |
30626 | 134 |
|
60731
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60729
diff
changeset
|
135 |
use "ML-Systems/ml_parse_tree.ML"; |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60729
diff
changeset
|
136 |
if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else (); |
4ac4b314d93c
additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents:
60729
diff
changeset
|
137 |
|
30626 | 138 |
|
60729 | 139 |
(* ML debugger *) |
140 |
||
141 |
use "ML-Systems/ml_debugger_dummy.ML"; |
|
142 |
if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_debugger_polyml-5.5.3.ML" else (); |
|
143 |
||
144 |
||
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
145 |
(* ML toplevel pretty printing *) |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
146 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
147 |
use "ML-Systems/ml_pretty.ML"; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
148 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
149 |
local |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
150 |
val depth = Unsynchronized.ref 10; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
151 |
in |
56281 | 152 |
fun get_default_print_depth () = ! depth; |
56285 | 153 |
fun default_print_depth n = (depth := n; PolyML.print_depth n); |
154 |
val _ = default_print_depth 10; |
|
47980
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
155 |
end; |
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
156 |
|
c81801f881b3
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents:
44249
diff
changeset
|
157 |
val error_depth = PolyML.error_depth; |
30626 | 158 |
|
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
159 |
val pretty_ml = |
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
160 |
let |
51638
1275716f395b
more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm
parents:
50911
diff
changeset
|
161 |
fun convert _ (PolyML.PrettyBreak (wd, _)) = ML_Pretty.Break (false, wd) |
54718 | 162 |
| convert _ (PolyML.PrettyBlock (_, _, |
51638
1275716f395b
more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm
parents:
50911
diff
changeset
|
163 |
[PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) = |
1275716f395b
more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm
parents:
50911
diff
changeset
|
164 |
ML_Pretty.Break (true, 1) |
1275716f395b
more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm
parents:
50911
diff
changeset
|
165 |
| convert len (PolyML.PrettyBlock (ind, _, context, prts)) = |
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
166 |
let |
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
167 |
fun property name default = |
31318 | 168 |
(case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of |
169 |
SOME (PolyML.ContextProperty (_, b)) => b |
|
54718 | 170 |
| _ => default); |
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
171 |
val bg = property "begin" ""; |
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
172 |
val en = property "end" ""; |
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
173 |
val len' = property "length" len; |
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
174 |
in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end |
31318 | 175 |
| convert len (PolyML.PrettyString s) = |
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
176 |
ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s) |
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
177 |
in convert "" end; |
30638 | 178 |
|
51638
1275716f395b
more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm
parents:
50911
diff
changeset
|
179 |
fun ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0) |
1275716f395b
more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm
parents:
50911
diff
changeset
|
180 |
| ml_pretty (ML_Pretty.Break (true, _)) = |
1275716f395b
more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm
parents:
50911
diff
changeset
|
181 |
PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")], |
1275716f395b
more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm
parents:
50911
diff
changeset
|
182 |
[PolyML.PrettyString " "]) |
1275716f395b
more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm
parents:
50911
diff
changeset
|
183 |
| ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) = |
30679 | 184 |
let val context = |
31318 | 185 |
(if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @ |
186 |
(if en = "" then [] else [PolyML.ContextProperty ("end", en)]) |
|
187 |
in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end |
|
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset
|
188 |
| ml_pretty (ML_Pretty.String (s, len)) = |
31318 | 189 |
if len = size s then PolyML.PrettyString s |
190 |
else PolyML.PrettyBlock |
|
51638
1275716f395b
more defensive representation of forced break within PolyML.PrettyBreak -- avoid accidental blowup if low-level operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm
parents:
50911
diff
changeset
|
191 |
(0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s]); |
30626 | 192 |
|
30673 | 193 |
fun toplevel_pp context (_: string list) pp = |
194 |
use_text context (1, "pp") false |
|
31318 | 195 |
("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))"); |
30626 | 196 |
|
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59055
diff
changeset
|
197 |
fun ml_make_string struct_name = |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59055
diff
changeset
|
198 |
"(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^ |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
59055
diff
changeset
|
199 |
struct_name ^ ".ML_print_depth ())))))"; |