| author | wenzelm |
| Thu, 17 Dec 2015 17:32:01 +0100 | |
| changeset 61862 | e2a9e46ac0fb |
| parent 38635 | f76ad0771f67 |
| child 61864 | 3a5992c3410c |
| permissions | -rw-r--r-- |
|
30622
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/ml_pretty.ML |
|
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 |
|
|
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
|
4 |
Minimal support for raw ML pretty printing -- for boot-strapping only. |
|
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 |
|
|
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
7 |
structure ML_Pretty = |
|
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
8 |
struct |
|
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
9 |
|
|
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
10 |
datatype pretty = |
|
30623
9ed1122d6cd2
simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
wenzelm
parents:
30622
diff
changeset
|
11 |
Block of (string * string) * pretty list * int | |
|
9ed1122d6cd2
simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
wenzelm
parents:
30622
diff
changeset
|
12 |
String of string * int | |
|
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
38635
diff
changeset
|
13 |
Break of bool * int * int; |
|
30622
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
14 |
|
|
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
|
15 |
fun block prts = Block (("", ""), prts, 2);
|
|
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
|
16 |
fun str s = String (s, size s); |
|
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
38635
diff
changeset
|
17 |
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
|
18 |
|
|
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
|
19 |
fun pair pretty1 pretty2 ((x, y), depth: int) = |
|
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
|
20 |
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
|
21 |
|
|
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
|
22 |
fun enum sep lpar rpar pretty (args, depth) = |
|
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
|
23 |
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
|
24 |
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
|
25 |
| 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
|
26 |
| 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
|
27 |
| elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs; |
|
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
|
28 |
in block (str lpar :: (elems (Int.max (depth, 0)) args @ [str rpar])) end; |
|
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
|
29 |
|
|
30622
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
30 |
end; |
|
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
31 |