author  wenzelm 
Thu, 17 Mar 2016 16:56:44 +0100  
changeset 62662  291cc01f56f5 
parent 62661  c23ff2f45a18 
child 62663  bea354f6ff21 
permissions  rwrr 
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62503
diff
changeset

1 
(* Title: Pure/ML/ml_pretty.ML 
30622
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset

2 
Author: Makarius 
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset

3 

62503  4 
Minimal support for raw ML pretty printing, notably for toplevel pp. 
30622
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset

5 
*) 
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset

6 

62503  7 
signature ML_PRETTY = 
8 
sig 

9 
datatype pretty = 

10 
Block of (string * string) * bool * FixedInt.int * pretty list  

11 
String of string * FixedInt.int  

12 
Break of bool * FixedInt.int * FixedInt.int 

13 
val block: pretty list > pretty 

14 
val str: string > pretty 

15 
val brk: FixedInt.int > pretty 

16 
val pair: ('a * int > pretty) > ('b * int > pretty) > ('a * 'b) * int > pretty 

17 
val enum: string > string > string > ('a * int > pretty) > 'a list * int > pretty 

18 
val to_polyml: pretty > PolyML.pretty 

19 
val from_polyml: PolyML.pretty > pretty 

62661  20 
val get_print_depth: unit > int 
21 
val print_depth: int > unit 

62662
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

22 
val format_polyml: int > PolyML.pretty > string 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

23 
val format: int > pretty > string 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

24 
val make_string_fn: string > string 
62503  25 
end; 
26 

27 
structure ML_Pretty: ML_PRETTY = 

30622
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset

28 
struct 
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset

29 

62661  30 
(* datatype pretty *) 
31 

30622
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset

32 
datatype pretty = 
62387
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset

33 
Block of (string * string) * bool * FixedInt.int * pretty list  
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset

34 
String of string * FixedInt.int  
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset

35 
Break of bool * FixedInt.int * FixedInt.int; 
30622
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset

36 

61869  37 
fun block prts = Block (("", ""), false, 2, prts); 
62387
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset

38 
fun str s = String (s, FixedInt.fromInt (size s)); 
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
38635
diff
changeset

39 
fun brk width = Break (false, width, 0); 
38635
f76ad0771f67
added ML toplevel prettyprinting for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
30623
diff
changeset

40 

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

41 
fun pair pretty1 pretty2 ((x, y), depth: FixedInt.int) = 
38635
f76ad0771f67
added ML toplevel prettyprinting for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
30623
diff
changeset

42 
block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth  1), str ")"]; 
f76ad0771f67
added ML toplevel prettyprinting for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
30623
diff
changeset

43 

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

44 
fun enum sep lpar rpar pretty (args, depth: FixedInt.int) = 
38635
f76ad0771f67
added ML toplevel prettyprinting for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
30623
diff
changeset

45 
let 
f76ad0771f67
added ML toplevel prettyprinting for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
30623
diff
changeset

46 
fun elems _ [] = [] 
f76ad0771f67
added ML toplevel prettyprinting for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
30623
diff
changeset

47 
 elems 0 _ = [str "..."] 
f76ad0771f67
added ML toplevel prettyprinting for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
30623
diff
changeset

48 
 elems d [x] = [pretty (x, d)] 
f76ad0771f67
added ML toplevel prettyprinting for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
30623
diff
changeset

49 
 elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d  1) xs; 
62387
ad3eb2889f9a
support for polymlgit ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset

50 
in block (str lpar :: (elems (FixedInt.max (depth, 0)) args @ [str rpar])) end; 
38635
f76ad0771f67
added ML toplevel prettyprinting for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
30623
diff
changeset

51 

62503  52 

53 
(* convert *) 

54 

55 
fun to_polyml (Break (false, width, offset)) = PolyML.PrettyBreak (width, offset) 

56 
 to_polyml (Break (true, _, _)) = 

57 
PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")], 

58 
[PolyML.PrettyString " "]) 

59 
 to_polyml (Block ((bg, en), consistent, ind, prts)) = 

60 
let val context = 

61 
(if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @ 

62 
(if en = "" then [] else [PolyML.ContextProperty ("end", en)]) 

63 
in PolyML.PrettyBlock (ind, consistent, context, map to_polyml prts) end 

64 
 to_polyml (String (s, len)) = 

65 
if len = FixedInt.fromInt (size s) then PolyML.PrettyString s 

66 
else 

67 
PolyML.PrettyBlock 

68 
(0, false, 

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

70 

71 
val from_polyml = 

72 
let 

73 
fun convert _ (PolyML.PrettyBreak (width, offset)) = Break (false, width, offset) 

74 
 convert _ (PolyML.PrettyBlock (_, _, 

75 
[PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) = 

76 
Break (true, 1, 0) 

77 
 convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) = 

78 
let 

79 
fun property name default = 

80 
(case List.find (fn PolyML.ContextProperty (a, _) => name = a  _ => false) context of 

81 
SOME (PolyML.ContextProperty (_, b)) => b 

82 
 _ => default); 

83 
val bg = property "begin" ""; 

84 
val en = property "end" ""; 

85 
val len' = property "length" len; 

86 
in Block ((bg, en), consistent, ind, map (convert len') prts) end 

87 
 convert len (PolyML.PrettyString s) = 

88 
String (s, FixedInt.fromInt (case Int.fromString len of SOME i => i  NONE => size s)) 

89 
in convert "" end; 

90 

62661  91 

92 
(* default print depth *) 

93 

94 
local 

95 
val depth = Unsynchronized.ref 0; 

96 
in 

97 
fun get_print_depth () = ! depth; 

98 
fun print_depth n = (depth := n; PolyML.print_depth n); 

99 
val _ = print_depth 10; 

30622
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset

100 
end; 
62661  101 

62662
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

102 

291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

103 
(* format *) 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

104 

291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

105 
fun format_polyml margin prt = 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

106 
let 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

107 
val result = Unsynchronized.ref []; 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

108 
val () = PolyML.prettyPrint (fn s => result := s :: ! result, margin) prt 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

109 
in String.concat (List.rev (! result)) end; 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

110 

291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

111 
fun format margin = format_polyml margin o to_polyml; 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

112 

291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

113 

291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

114 
(* make string *) 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

115 

291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

116 
local 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

117 
fun pretty_string_of s = 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

118 
"(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (" ^ s ^ "))))"; 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

119 
fun pretty_value depth = "PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ depth ^ "))"; 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

120 
in 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

121 

291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

122 
fun make_string_fn local_env = 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

123 
if local_env <> "" then 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

124 
pretty_string_of (pretty_value (local_env ^ ".ML_print_depth ()")) 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

125 
else if List.exists (fn (a, _) => a = "Pretty") (#allStruct ML_Name_Space.global ()) then 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

126 
pretty_string_of (pretty_value "ML_Pretty.get_print_depth ()") 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

127 
else "(fn x => ML_Pretty.format_polyml 78 (" ^ pretty_value "ML_Pretty.get_print_depth ()" ^ "))"; 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

128 

62661  129 
end; 
62662
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

130 

291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset

131 
end; 