author  wenzelm 
Thu, 24 May 2012 15:54:38 +0200  
changeset 47986  ca7104aebb74 
parent 43761  e72ba84ae58f 
parent 47980  c81801f881b3 
child 50910  54f06ba192ef 
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 

47980
c81801f881b3
simplified Poly/ML setup  5.3.0 is now the common baseline;
wenzelm
parents:
43791
diff
changeset

4 
Extra toplevel prettyprinting for Poly/ML 5.3.0 or later. 
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 ^ " (") ")"; 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

34 
fun prt_term parens dp (t as _ $ _) = 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

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

36 
> map_index (fn (i, u) => prt_term true (dp  i  1) u) 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

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

38 
> (if parens then Pretty.enclose "(" ")" else Pretty.block) 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

39 
 prt_term _ dp (Abs (x, T, body)) = 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

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

41 
[from_ML (prettyRepresentation (x, dp  1)), 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

42 
from_ML (prettyRepresentation (T, dp  2)), 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

43 
prt_term false (dp  3) body] 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

44 
 prt_term _ dp (Const const) = 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

45 
prt_app "Const" (from_ML (prettyRepresentation (const, dp  1))) 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

46 
 prt_term _ dp (Free free) = 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

47 
prt_app "Free" (from_ML (prettyRepresentation (free, dp  1))) 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

48 
 prt_term _ dp (Var var) = 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

49 
prt_app "Var" (from_ML (prettyRepresentation (var, dp  1))) 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

50 
 prt_term _ dp (Bound i) = 
d8903f0002e5
homegrown pretty printer for term  Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents:
33538
diff
changeset

51 
prt_app "Bound" (from_ML (prettyRepresentation (i, dp  1))); 
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 