author | wenzelm |
Thu, 17 Mar 2016 13:44:18 +0100 | |
changeset 62661 | c23ff2f45a18 |
parent 62508 | d0b68218ea55 |
child 62662 | 291cc01f56f5 |
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 |
|
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 polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset
|
30 |
Block of (string * string) * bool * FixedInt.int * pretty list | |
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset
|
31 |
String of string * FixedInt.int | |
ad3eb2889f9a
support for polyml-git 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 polyml-git 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 pretty-printing 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 polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset
|
38 |
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
|
39 |
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
|
40 |
|
62387
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
61925
diff
changeset
|
41 |
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
|
42 |
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
|
43 |
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
|
44 |
| 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
|
45 |
| 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
|
46 |
| 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
|
47 |
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
|
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; |