author  wenzelm 
Thu, 17 Mar 2016 13:44:18 +0100  
changeset 62661  c23ff2f45a18 
parent 62508  d0b68218ea55 
child 62662  291cc01f56f5 
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 

62503  22 
end; 
23 

24 
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

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

26 

62661  27 
(* datatype pretty *) 
28 

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

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

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

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

32 
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

33 

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

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

36 
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

37 

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

38 
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

39 
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

40 

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

41 
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

42 
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

43 
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

44 
 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

45 
 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

46 
 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

47 
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

48 

62503  49 

50 
(* convert *) 

51 

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

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

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

55 
[PolyML.PrettyString " "]) 

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

57 
let val context = 

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

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

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

61 
 to_polyml (String (s, len)) = 

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

63 
else 

64 
PolyML.PrettyBlock 

65 
(0, false, 

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

67 

68 
val from_polyml = 

69 
let 

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

71 
 convert _ (PolyML.PrettyBlock (_, _, 

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

73 
Break (true, 1, 0) 

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

75 
let 

76 
fun property name default = 

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

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

79 
 _ => default); 

80 
val bg = property "begin" ""; 

81 
val en = property "end" ""; 

82 
val len' = property "length" len; 

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

84 
 convert len (PolyML.PrettyString s) = 

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

86 
in convert "" end; 

87 

62661  88 

89 
(* default print depth *) 

90 

91 
local 

92 
val depth = Unsynchronized.ref 0; 

93 
in 

94 
fun get_print_depth () = ! depth; 

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

96 
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

97 
end; 
62661  98 

99 
end; 