author  wenzelm 
Tue, 24 Mar 2009 23:43:58 +0100  
changeset 30714  88bc86d7dec3 
parent 30633  cc18ae3c1c7f 
child 31311  b82e55f51dcc 
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 

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

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

4 
Poly/ML 5.3. 
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 

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

7 
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

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

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

10 
 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

11 
 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

12 

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

13 
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 Lazy.peek x of 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

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

16 
 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

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 