author | wenzelm |
Mon, 17 Oct 2016 15:46:51 +0200 | |
changeset 64275 | ac2abc987cf9 |
parent 62900 | c641bf9402fd |
child 68918 | 3a0db30e5d87 |
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 |
|
62784
0371c369ab1d
adapted to Poly/ML repository version 2e40cadc975a;
wenzelm
parents:
62711
diff
changeset
|
16 |
val pair: ('a * FixedInt.int -> pretty) -> ('b * FixedInt.int -> pretty) -> |
0371c369ab1d
adapted to Poly/ML repository version 2e40cadc975a;
wenzelm
parents:
62711
diff
changeset
|
17 |
('a * 'b) * FixedInt.int -> pretty |
0371c369ab1d
adapted to Poly/ML repository version 2e40cadc975a;
wenzelm
parents:
62711
diff
changeset
|
18 |
val enum: string -> string -> string -> ('a * FixedInt.int -> pretty) -> |
0371c369ab1d
adapted to Poly/ML repository version 2e40cadc975a;
wenzelm
parents:
62711
diff
changeset
|
19 |
'a list * FixedInt.int -> pretty |
62823 | 20 |
val to_polyml: pretty -> PolyML_Pretty.pretty |
21 |
val from_polyml: PolyML_Pretty.pretty -> pretty |
|
22 |
val format_polyml: int -> PolyML_Pretty.pretty -> string |
|
62662
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
23 |
val format: int -> pretty -> string |
62899
845ed4584e21
clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents:
62878
diff
changeset
|
24 |
val default_margin: int |
845ed4584e21
clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents:
62878
diff
changeset
|
25 |
val string_of_polyml: PolyML_Pretty.pretty -> string |
62900
c641bf9402fd
simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
wenzelm
parents:
62899
diff
changeset
|
26 |
val make_string_fn: string |
62503 | 27 |
end; |
28 |
||
29 |
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
|
30 |
struct |
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
31 |
|
62661 | 32 |
(* datatype pretty *) |
33 |
||
30622
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
34 |
datatype pretty = |
62387
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset
|
35 |
Block of (string * string) * bool * FixedInt.int * pretty list | |
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset
|
36 |
String of string * FixedInt.int | |
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset
|
37 |
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
|
38 |
|
61869 | 39 |
fun block prts = Block (("", ""), false, 2, prts); |
62387
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset
|
40 |
fun str s = String (s, FixedInt.fromInt (size s)); |
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
38635
diff
changeset
|
41 |
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
|
42 |
|
62387
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset
|
43 |
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
|
44 |
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
|
45 |
|
62387
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset
|
46 |
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
|
47 |
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
|
48 |
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
|
49 |
| 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
|
50 |
| 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
|
51 |
| 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
|
52 |
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
|
53 |
|
62503 | 54 |
|
55 |
(* convert *) |
|
56 |
||
62823 | 57 |
fun to_polyml (Break (false, width, offset)) = PolyML_Pretty.PrettyBreak (width, offset) |
62503 | 58 |
| to_polyml (Break (true, _, _)) = |
62823 | 59 |
PolyML_Pretty.PrettyBlock (0, false, [PolyML_Pretty.ContextProperty ("fbrk", "")], |
60 |
[PolyML_Pretty.PrettyString " "]) |
|
62503 | 61 |
| to_polyml (Block ((bg, en), consistent, ind, prts)) = |
62 |
let val context = |
|
62823 | 63 |
(if bg = "" then [] else [PolyML_Pretty.ContextProperty ("begin", bg)]) @ |
64 |
(if en = "" then [] else [PolyML_Pretty.ContextProperty ("end", en)]) |
|
65 |
in PolyML_Pretty.PrettyBlock (ind, consistent, context, map to_polyml prts) end |
|
62503 | 66 |
| to_polyml (String (s, len)) = |
62823 | 67 |
if len = FixedInt.fromInt (size s) then PolyML_Pretty.PrettyString s |
62503 | 68 |
else |
62823 | 69 |
PolyML_Pretty.PrettyBlock |
62503 | 70 |
(0, false, |
62823 | 71 |
[PolyML_Pretty.ContextProperty ("length", FixedInt.toString len)], [PolyML_Pretty.PrettyString s]); |
62503 | 72 |
|
73 |
val from_polyml = |
|
74 |
let |
|
62823 | 75 |
fun convert _ (PolyML_Pretty.PrettyBreak (width, offset)) = Break (false, width, offset) |
76 |
| convert _ (PolyML_Pretty.PrettyBlock (_, _, |
|
77 |
[PolyML_Pretty.ContextProperty ("fbrk", _)], [PolyML_Pretty.PrettyString " "])) = |
|
62503 | 78 |
Break (true, 1, 0) |
62823 | 79 |
| convert len (PolyML_Pretty.PrettyBlock (ind, consistent, context, prts)) = |
62503 | 80 |
let |
81 |
fun property name default = |
|
62823 | 82 |
(case List.find (fn PolyML_Pretty.ContextProperty (a, _) => name = a | _ => false) context of |
83 |
SOME (PolyML_Pretty.ContextProperty (_, b)) => b |
|
62503 | 84 |
| _ => default); |
85 |
val bg = property "begin" ""; |
|
86 |
val en = property "end" ""; |
|
87 |
val len' = property "length" len; |
|
88 |
in Block ((bg, en), consistent, ind, map (convert len') prts) end |
|
62823 | 89 |
| convert len (PolyML_Pretty.PrettyString s) = |
62503 | 90 |
String (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s)) |
91 |
in convert "" end; |
|
92 |
||
62661 | 93 |
|
62662
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
94 |
(* format *) |
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
95 |
|
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
96 |
fun format_polyml margin prt = |
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
97 |
let |
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
98 |
val result = Unsynchronized.ref []; |
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
99 |
val () = PolyML.prettyPrint (fn s => result := s :: ! result, margin) prt |
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
100 |
in String.concat (List.rev (! result)) end; |
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
101 |
|
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
102 |
fun format margin = format_polyml margin o to_polyml; |
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
103 |
|
62899
845ed4584e21
clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents:
62878
diff
changeset
|
104 |
val default_margin = 76; |
845ed4584e21
clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents:
62878
diff
changeset
|
105 |
|
62662
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
106 |
|
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
107 |
(* make string *) |
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
108 |
|
62899
845ed4584e21
clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents:
62878
diff
changeset
|
109 |
val string_of_polyml = format_polyml default_margin; |
62662
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
110 |
|
62900
c641bf9402fd
simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
wenzelm
parents:
62899
diff
changeset
|
111 |
val make_string_fn = |
c641bf9402fd
simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
wenzelm
parents:
62899
diff
changeset
|
112 |
"(fn x => ML_Pretty.string_of_polyml (ML_system_pretty \ |
c641bf9402fd
simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
wenzelm
parents:
62899
diff
changeset
|
113 |
\(x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()))))"; |
62662
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62661
diff
changeset
|
114 |
|
62661 | 115 |
end; |