author  wenzelm 
Sun, 31 May 2009 14:46:44 +0200  
changeset 31311  b82e55f51dcc 
parent 30714  88bc86d7dec3 
child 31318  133d1cfd6ae7 
permissions  rwrr 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/MLSystems/install_pp_polymlexperimental.ML 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

2 

31311  3 
Extra toplevel prettyprinting for Poly/ML 5.3 (SVN experimental). 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

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

5 

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

6 
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

7 
(case Future.peek x of 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

8 
NONE => PrettyString "<future>" 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

9 
 SOME (Exn.Exn _) => 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

10 
 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

11 

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

12 
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

13 
(case Lazy.peek x of 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

14 
NONE => PrettyString "<lazy>" 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

15 
 SOME (Exn.Exn _) => 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

16 
 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

17 