author | wenzelm |
Fri, 18 Mar 2016 21:21:09 +0100 | |
changeset 62672 | 068b430e678f |
parent 62663 | bea354f6ff21 |
child 62711 | 09df6a51ad3c |
permissions | -rw-r--r-- |
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 polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset
|
33 |
Block of (string * string) * bool * FixedInt.int * pretty list | |
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset
|
34 |
String of string * FixedInt.int | |
ad3eb2889f9a
support for polyml-git 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 polyml-git 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 pretty-printing 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 polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset
|
41 |
fun pair pretty1 pretty2 ((x, y), depth: FixedInt.int) = |
38635
f76ad0771f67
added ML toplevel pretty-printing 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 pretty-printing 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 polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset
|
44 |
fun enum sep lpar rpar pretty (args, depth: FixedInt.int) = |
38635
f76ad0771f67
added ML toplevel pretty-printing 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 pretty-printing 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 pretty-printing 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 pretty-printing 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 pretty-printing 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 polyml-git 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 pretty-printing 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); |
|
62672 | 99 |
val _ = print_depth 20; |
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 |
62663 | 117 |
fun pretty_string_of s = "(fn x => Pretty.string_of (Pretty.from_polyml (" ^ s ^ ")))"; |
62662
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
118 |
fun pretty_value depth = "PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ depth ^ "))"; |
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
119 |
in |
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
120 |
|
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
121 |
fun make_string_fn local_env = |
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
122 |
if local_env <> "" then |
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
123 |
pretty_string_of (pretty_value (local_env ^ ".ML_print_depth ()")) |
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
124 |
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
|
125 |
pretty_string_of (pretty_value "ML_Pretty.get_print_depth ()") |
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
126 |
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
|
127 |
|
62661 | 128 |
end; |
62662
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
129 |
|
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
130 |
end; |