author  wenzelm 
Sat, 19 Dec 2015 19:52:52 +0100  
changeset 61869  ba466ac335e3 
parent 61864  3a5992c3410c 
permissions  rwrr 
30622
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/MLSystems/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 prettyprinting 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 bootstrapping 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 = 
61869  11 
Block of (string * string) * bool * int * pretty list  
30623
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 

61869  15 
fun block prts = Block (("", ""), false, 2, prts); 
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

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 prettyprinting 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 prettyprinting 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 prettyprinting 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 prettyprinting 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 prettyprinting 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 prettyprinting 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 prettyprinting 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 prettyprinting 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 prettyprinting 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 prettyprinting 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 prettyprinting 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 prettyprinting 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; 