author  wenzelm 
Wed, 29 Dec 2010 20:41:33 +0100  
changeset 41415  23533273220a 
parent 38327  d6afb77b0f6d 
child 43761  e72ba84ae58f 
permissions  rwrr 
38327  1 
(* Title: Pure/ML/install_pp_polyml5.3.ML 
2 
Author: Makarius 

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

3 

33538
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
31433
diff
changeset

4 
Extra toplevel prettyprinting for Poly/ML 5.3.0. 
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 

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

12 

31318  13 
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

14 
(case Future.peek x of 
31318  15 
NONE => PolyML.PrettyString "<future>" 
16 
 SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" 

30714
88bc86d7dec3
simplified addPrettyPrinter setup: may pass (fn ...) directly if type constraints are omitted  addPrettyPrinter treated as a special case internally;
wenzelm
parents:
30633
diff
changeset

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

18 

31318  19 
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

20 
(case Lazy.peek x of 
31318  21 
NONE => PolyML.PrettyString "<lazy>" 
22 
 SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" 

30714
88bc86d7dec3
simplified addPrettyPrinter setup: may pass (fn ...) directly if type constraints are omitted  addPrettyPrinter treated as a special case internally;
wenzelm
parents:
30633
diff
changeset

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

24 

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

25 
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

26 
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

27 
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

28 
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

29 
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

30 
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

31 
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

32 
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

33 
> 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

34 
> 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

35 
> (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

36 
 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

37 
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

38 
[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

39 
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

40 
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

41 
 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

42 
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

43 
 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

44 
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

45 
 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

46 
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

47 
 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

48 
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

49 
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

50 