author  wenzelm 
Thu, 01 Aug 2013 23:10:46 +0200  
changeset 52837  fe1f6a1707f7 
parent 52711  155f02cacb2d 
child 53709  84522727f9d3 
permissions  rwrr 
33538
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
32778
diff
changeset

1 
(* Title: Pure/MLSystems/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 

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

7 
(* exceptions *) 
30673  8 

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

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

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

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

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

13 

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

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

15 

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

16 
use "General/exn.ML"; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

17 

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

18 

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

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

20 

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

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

22 

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

23 
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

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

25 
else use "MLSystems/single_assignment_polyml.ML"; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

26 

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

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

28 
use "MLSystems/multithreading.ML"; 
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

29 
use "MLSystems/multithreading_polyml.ML"; 
47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

30 

39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38470
diff
changeset

31 
use "MLSystems/unsynchronized.ML"; 
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38470
diff
changeset

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

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

34 

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

35 

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

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

37 

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

38 
fun op before (a, _: unit) = a; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

39 

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

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

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

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

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

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

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

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

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

48 

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

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

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

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

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

53 

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

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

55 

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

56 

48416  57 
(* ML system operations *) 
47980
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 
use "MLSystems/ml_system.ML"; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

60 

52711
155f02cacb2d
old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
wenzelm
parents:
51638
diff
changeset

61 
if ML_System.name = "polyml5.3.0" 
155f02cacb2d
old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
wenzelm
parents:
51638
diff
changeset

62 
then use "MLSystems/share_common_data_polyml5.3.0.ML" 
155f02cacb2d
old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
wenzelm
parents:
51638
diff
changeset

63 
else (); 
155f02cacb2d
old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
wenzelm
parents:
51638
diff
changeset

64 

48416  65 
structure ML_System = 
66 
struct 

67 

68 
open ML_System; 

69 

70 
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; 

71 
val save_state = PolyML.SaveState.saveState; 

72 

73 
end; 

74 

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

75 

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

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

77 

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

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

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

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

81 

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

82 
fun profile 0 f x = f x 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

83 
 profile n f x = 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

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

85 
val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

86 
val res = Exn.capture f x; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

87 
val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

88 
in Exn.release res end; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

89 

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

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

91 

47980
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 
(* ML compiler *) 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

94 

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

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

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

97 
open PolyML.NameSpace; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

98 
type T = PolyML.NameSpace.nameSpace; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

99 
val global = PolyML.globalNameSpace; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

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

101 

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

102 
use "MLSystems/use_context.ML"; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

103 
use "MLSystems/compiler_polyml.ML"; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

104 

32778  105 
PolyML.Compiler.reportUnreferencedIds := true; 
47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

106 
PolyML.Compiler.printInAlphabeticalOrder := false; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

107 
PolyML.Compiler.maxInlineSize := 80; 
52837  108 
(*PolyML.Compiler.reportExhaustiveHandlers := true;*) 
47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

109 

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

110 
fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); 
30626  111 

112 

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

113 
(* ML toplevel pretty printing *) 
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 
use "MLSystems/ml_pretty.ML"; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

116 

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

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

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

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

120 
fun get_print_depth () = ! depth; 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

121 
fun print_depth n = (depth := n; PolyML.print_depth n); 
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
44249
diff
changeset

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

123 

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

124 
val error_depth = PolyML.error_depth; 
30626  125 

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

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

127 
let 
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

128 
fun convert _ (PolyML.PrettyBreak (wd, _)) = ML_Pretty.Break (false, wd) 
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

129 
 convert _ (PolyML.PrettyBlock (ind, _, 
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

130 
[PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) = 
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

131 
ML_Pretty.Break (true, 1) 
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

132 
 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

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

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

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

137 
 NONE => default); 
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset

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

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

140 
val len' = property "length" len; 
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset

141 
in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end 
31318  142 
 convert len (PolyML.PrettyString s) = 
30676
edca392a2abb
pretty_ml/ml_pretty: proper handling of markup and string length;
wenzelm
parents:
30673
diff
changeset

143 
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

144 
in convert "" end; 
30638  145 

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

146 
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 lowlevel operations are used, notably PolyML.makestring or its variant General.exnMessage;
wenzelm
parents:
50911
diff
changeset

147 
 ml_pretty (ML_Pretty.Break (true, _)) = 
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

148 
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

149 
[PolyML.PrettyString " "]) 
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

150 
 ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) = 
30679  151 
let val context = 
31318  152 
(if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @ 
153 
(if en = "" then [] else [PolyML.ContextProperty ("end", en)]) 

154 
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

155 
 ml_pretty (ML_Pretty.String (s, len)) = 
31318  156 
if len = size s then PolyML.PrettyString s 
157 
else 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

158 
(0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s]); 
30626  159 

30673  160 
fun toplevel_pp context (_: string list) pp = 
161 
use_text context (1, "pp") false 

31318  162 
("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))"); 
30626  163 

36162
0bd034a80a9a
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
wenzelm
parents:
33543
diff
changeset

164 
val ml_make_string = 
0bd034a80a9a
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
wenzelm
parents:
33543
diff
changeset

165 
"(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, get_print_depth ())))))"; 
0bd034a80a9a
added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
wenzelm
parents:
33543
diff
changeset

166 