author  wenzelm 
Tue, 01 Mar 2016 19:42:59 +0100  
changeset 62490  39d01eaf5292 
parent 62472  01e2bd5b4027 
child 62493  dd154240a53c 
permissions  rwrr 
62077  1 
(* Title: Pure/RAW/ROOT_polyml.ML 
47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
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 

60953
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset

7 
(* initial ML name space *) 
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset

8 

61925  9 
use "RAW/ml_system.ML"; 
61715
5dc95d957569
speculative support for polyml5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
60993
diff
changeset

10 

5dc95d957569
speculative support for polyml5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
60993
diff
changeset

11 
if ML_System.name = "polyml5.6" 
61925  12 
then use "RAW/ml_name_space_polyml5.6.ML" 
13 
else use "RAW/ml_name_space_polyml.ML"; 

61715
5dc95d957569
speculative support for polyml5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
60993
diff
changeset

14 

62387
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset

15 
if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then () 
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset

16 
else use "RAW/fixed_int_dummy.ML"; 
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset

17 

60953
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset

18 
structure ML_Name_Space = 
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset

19 
struct 
61715
5dc95d957569
speculative support for polyml5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
60993
diff
changeset

20 
open ML_Name_Space; 
60953
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset

21 
val initial_val = 
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset

22 
List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit") 
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset

23 
(#allVal global ()); 
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset

24 
val initial_type = #allType global (); 
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset

25 
val initial_fixity = #allFix global (); 
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset

26 
val initial_structure = #allStruct global (); 
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset

27 
val initial_signature = #allSig global (); 
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset

28 
val initial_functor = #allFunct global (); 
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset

29 
end; 
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML addons;
wenzelm
parents:
54723
diff
changeset

30 

600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML addons;
wenzelm
parents:
54723
diff
changeset

31 

62467  32 
(* ML heap operations *) 
54717  33 

62467  34 
if ML_System.name = "polyml5.3.0" 
35 
then use "RAW/ml_heap_polyml5.3.0.ML" 

36 
else use "RAW/ml_heap.ML"; 

54717  37 

38 

47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

39 
(* exceptions *) 
30673  40 

31427
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset

41 
fun reraise exn = 
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset

42 
(case PolyML.exceptionLocation exn of 
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset

43 
NONE => raise exn 
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset

44 
 SOME location => PolyML.raiseWithLocation (exn, location)); 
5a07cc86675d
reraise exceptions to preserve original position (ML system specific);
wenzelm
parents:
31318
diff
changeset

45 

47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

46 
exception Interrupt = SML90.Interrupt; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

47 

61925  48 
use "RAW/exn.ML"; 
47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

49 

62459  50 
if ML_System.name = "polyml5.6" 
51 
then use "RAW/exn_trace.ML" 

62460  52 
else use "RAW/exn_trace_raw.ML"; 
59470  53 

47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

54 

c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

55 
(* multithreading *) 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

56 

c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

57 
val seconds = Time.fromReal; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

58 

c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

59 
if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ()) 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

60 
then () 
61925  61 
else use "RAW/single_assignment_polyml.ML"; 
47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

62 

c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

63 
open Thread; 
61925  64 
use "RAW/multithreading.ML"; 
47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

65 

61794
4c232a2ddeab
discontinued intermediate polyml5.5.3, assuming the coming release will be polyml5.6;
wenzelm
parents:
61715
diff
changeset

66 
if ML_System.name = "polyml5.6" 
61925  67 
then use "RAW/ml_stack_polyml5.6.ML" 
68 
else use "RAW/ml_stack_dummy.ML"; 

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

69 

61925  70 
use "RAW/unsynchronized.ML"; 
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38470
diff
changeset

71 
val _ = PolyML.Compiler.forgetValue "ref"; 
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38470
diff
changeset

72 
val _ = PolyML.Compiler.forgetType "ref"; 
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

73 

47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

74 

c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

75 
(* pervasive environment *) 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

76 

c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

77 
val _ = PolyML.Compiler.forgetValue "isSome"; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

78 
val _ = PolyML.Compiler.forgetValue "getOpt"; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

79 
val _ = PolyML.Compiler.forgetValue "valOf"; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

80 
val _ = PolyML.Compiler.forgetValue "foldl"; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

81 
val _ = PolyML.Compiler.forgetValue "foldr"; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

82 
val _ = PolyML.Compiler.forgetValue "print"; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

83 
val _ = PolyML.Compiler.forgetValue "explode"; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

84 
val _ = PolyML.Compiler.forgetValue "concat"; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

85 

c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

86 
val ord = SML90.ord; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

87 
val chr = SML90.chr; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

88 
val raw_explode = SML90.explode; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

89 
val implode = SML90.implode; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

90 

c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

91 
fun quit () = exit 0; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

92 

c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

93 

c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

94 
(* ML runtime system *) 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

95 

61715
5dc95d957569
speculative support for polyml5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
60993
diff
changeset

96 
if ML_System.name = "polyml5.6" 
61925  97 
then use "RAW/ml_profiling_polyml5.6.ML" 
98 
else use "RAW/ml_profiling_polyml.ML"; 

47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

99 

29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

100 
val pointer_eq = PolyML.pointerEq; 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

101 

47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

102 

c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

103 
(* ML toplevel pretty printing *) 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

104 

61925  105 
use "RAW/ml_pretty.ML"; 
47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

106 

c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

107 
local 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

108 
val depth = Unsynchronized.ref 10; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

109 
in 
56281  110 
fun get_default_print_depth () = ! depth; 
56285  111 
fun default_print_depth n = (depth := n; PolyML.print_depth n); 
112 
val _ = default_print_depth 10; 

47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

113 
end; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

114 

c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

115 
val error_depth = PolyML.error_depth; 
30626  116 

30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset

117 
val pretty_ml = 
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset

118 
let 
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61794
diff
changeset

119 
fun convert _ (PolyML.PrettyBreak (width, offset)) = ML_Pretty.Break (false, width, offset) 
54718  120 
 convert _ (PolyML.PrettyBlock (_, _, 
51638
1275716f395b
more defensive representation of forced break within PolyML.PrettyBreak  avoid accidental blowup if lowlevel operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm
parents:
50911
diff
changeset

121 
[PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) = 
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61794
diff
changeset

122 
ML_Pretty.Break (true, 1, 0) 
61864  123 
 convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) = 
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset

124 
let 
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset

125 
fun property name default = 
31318  126 
(case List.find (fn PolyML.ContextProperty (a, _) => name = a  _ => false) context of 
127 
SOME (PolyML.ContextProperty (_, b)) => b 

54718  128 
 _ => default); 
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset

129 
val bg = property "begin" ""; 
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset

130 
val en = property "end" ""; 
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset

131 
val len' = property "length" len; 
61869  132 
in ML_Pretty.Block ((bg, en), consistent, ind, map (convert len') prts) end 
31318  133 
 convert len (PolyML.PrettyString s) = 
62387
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset

134 
ML_Pretty.String 
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset

135 
(s, FixedInt.fromInt (case Int.fromString len of SOME i => i  NONE => size s)) 
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset

136 
in convert "" end; 
30638  137 

61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61794
diff
changeset

138 
fun ml_pretty (ML_Pretty.Break (false, width, offset)) = PolyML.PrettyBreak (width, offset) 
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61794
diff
changeset

139 
 ml_pretty (ML_Pretty.Break (true, _, _)) = 
51638
1275716f395b
more defensive representation of forced break within PolyML.PrettyBreak  avoid accidental blowup if lowlevel operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm
parents:
50911
diff
changeset

140 
PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")], 
1275716f395b
more defensive representation of forced break within PolyML.PrettyBreak  avoid accidental blowup if lowlevel operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm
parents:
50911
diff
changeset

141 
[PolyML.PrettyString " "]) 
61869  142 
 ml_pretty (ML_Pretty.Block ((bg, en), consistent, ind, prts)) = 
30679  143 
let val context = 
31318  144 
(if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @ 
145 
(if en = "" then [] else [PolyML.ContextProperty ("end", en)]) 

61864  146 
in PolyML.PrettyBlock (ind, consistent, context, map ml_pretty prts) end 
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset

147 
 ml_pretty (ML_Pretty.String (s, len)) = 
62387
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset

148 
if len = FixedInt.fromInt (size s) then PolyML.PrettyString s 
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset

149 
else 
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset

150 
PolyML.PrettyBlock 
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset

151 
(0, false, 
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset

152 
[PolyML.ContextProperty ("length", FixedInt.toString len)], [PolyML.PrettyString s]); 
30626  153 

60897  154 

155 
(* ML compiler *) 

156 

157 
structure ML_Name_Space = 

158 
struct 

60953
87f0f707a5f8
clarified initial ML name space (amending 7aad4be8a48e);
wenzelm
parents:
60923
diff
changeset

159 
open ML_Name_Space; 
61715
5dc95d957569
speculative support for polyml5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
60993
diff
changeset

160 
val display_val = pretty_ml o displayVal; 
60897  161 
end; 
162 

61925  163 
use "RAW/ml_compiler_parameters.ML"; 
61794
4c232a2ddeab
discontinued intermediate polyml5.5.3, assuming the coming release will be polyml5.6;
wenzelm
parents:
61715
diff
changeset

164 
if ML_System.name = "polyml5.6" 
61925  165 
then use "RAW/ml_compiler_parameters_polyml5.6.ML" else (); 
60956  166 

61925  167 
use "RAW/ml_positions.ML"; 
168 
use "RAW/compiler_polyml.ML"; 

60897  169 

170 
PolyML.Compiler.reportUnreferencedIds := true; 

171 
PolyML.Compiler.printInAlphabeticalOrder := false; 

172 
PolyML.Compiler.maxInlineSize := 80; 

62472  173 
PolyML.Compiler.prompt1 := "ML> "; 
174 
PolyML.Compiler.prompt2 := "ML# "; 

60897  175 

61925  176 
use "RAW/ml_parse_tree.ML"; 
61794
4c232a2ddeab
discontinued intermediate polyml5.5.3, assuming the coming release will be polyml5.6;
wenzelm
parents:
61715
diff
changeset

177 
if ML_System.name = "polyml5.6" 
61925  178 
then use "RAW/ml_parse_tree_polyml5.6.ML" else (); 
60897  179 

59127
723b11f8ffbf
more careful handling of auxiliary environment structure  allow nested ML evaluation;
wenzelm
parents:
59055
diff
changeset

180 
fun ml_make_string struct_name = 
62387
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset

181 
"(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ 
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62359
diff
changeset

182 
struct_name ^ ".ML_print_depth ()))))))"; 
60897  183 

184 

185 
(* ML debugger *) 

186 

61794
4c232a2ddeab
discontinued intermediate polyml5.5.3, assuming the coming release will be polyml5.6;
wenzelm
parents:
61715
diff
changeset

187 
if ML_System.name = "polyml5.6" 
62490
39d01eaf5292
ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents:
62472
diff
changeset

188 
then use_no_debug "RAW/ml_debugger_polyml5.6.ML" 
39d01eaf5292
ML debugger support in Pure (again, see 3565c9f407ec);
wenzelm
parents:
62472
diff
changeset

189 
else use_no_debug "RAW/ml_debugger.ML"; 