author  wenzelm 
Sun, 23 Jun 2013 17:14:20 +0200  
changeset 52425  de8a85aad216 
parent 50910  54f06ba192ef 
child 52426  81e27230a8b7 
permissions  rwrr 
47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
43791
diff
changeset

1 
(* Title: Pure/ML/install_pp_polyml.ML 
38327  2 
Author: Makarius 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

3 

50910  4 
Extra toplevel prettyprinting for Poly/ML. 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

5 
*) 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

6 

41415
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
38327
diff
changeset

7 
PolyML.addPrettyPrinter (fn depth => fn _ => fn str => 
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
38327
diff
changeset

8 
ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str))); 
23533273220a
tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents:
38327
diff
changeset

9 

43791  10 
PolyML.addPrettyPrinter (fn depth => fn _ => fn tree => 
11 
ml_pretty (Pretty.to_ML (XML.pretty depth tree))); 

12 

33767  13 
PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => 
14 
pretty (Synchronized.value var, depth)); 

15 

31318  16 
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

17 
(case Future.peek x of 
31318  18 
NONE => PolyML.PrettyString "<future>" 
19 
 SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" 

43761
e72ba84ae58f
tuned signature  corresponding to Scala version;
wenzelm
parents:
41415
diff
changeset

20 
 SOME (Exn.Res y) => pretty (y, depth))); 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

21 

31318  22 
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

23 
(case Lazy.peek x of 
31318  24 
NONE => PolyML.PrettyString "<lazy>" 
25 
 SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" 

43761
e72ba84ae58f
tuned signature  corresponding to Scala version;
wenzelm
parents:
41415
diff
changeset

26 
 SOME (Exn.Res y) => pretty (y, depth))); 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

27 

33545
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

28 
PolyML.addPrettyPrinter (fn depth => fn _ => fn tm => 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

29 
let 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

30 
open PolyML; 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

31 
val from_ML = Pretty.from_ML o pretty_ml; 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

32 
fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt]; 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

33 
fun prt_apps name = Pretty.enum "," (name ^ " (") ")"; 
52425
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

34 
fun prt_term parens dp t = 
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

35 
if dp <= 0 then Pretty.str "..." 
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

36 
else 
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

37 
(case t of 
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

38 
_ $ _ => 
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

39 
op :: (strip_comb t) 
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

40 
> map_index (fn (i, u) => prt_term true (dp  i  1) u) 
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

41 
> Pretty.separate " $" 
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

42 
> (if parens then Pretty.enclose "(" ")" else Pretty.block) 
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

43 
 Abs (a, T, b) => 
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

44 
prt_apps "Abs" 
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

45 
[from_ML (prettyRepresentation (a, dp  1)), 
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

46 
from_ML (prettyRepresentation (T, dp  2)), 
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

47 
prt_term false (dp  3) b] 
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

48 
 Const const => prt_app "Const" (from_ML (prettyRepresentation (const, dp  1))) 
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

49 
 Free free => prt_app "Free" (from_ML (prettyRepresentation (free, dp  1))) 
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

50 
 Var var => prt_app "Var" (from_ML (prettyRepresentation (var, dp  1))) 
de8a85aad216
actually observe print_depth for outer term structure;
wenzelm
parents:
50910
diff
changeset

51 
 Bound i => prt_app "Bound" (from_ML (prettyRepresentation (i, dp  1)))); 
33545
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

52 
in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end); 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

53 