| author | wenzelm |
| Sun, 31 May 2009 16:29:39 +0200 | |
| changeset 31318 | 133d1cfd6ae7 |
| parent 31311 | b82e55f51dcc |
| permissions | -rw-r--r-- |
|
30633
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/install_pp_polyml-experimental.ML |
|
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
2 |
|
| 31311 | 3 |
Extra toplevel pretty-printing for Poly/ML 5.3 (SVN experimental). |
|
30633
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
4 |
*) |
|
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
5 |
|
| 31318 | 6 |
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => |
|
30633
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
7 |
(case Future.peek x of |
| 31318 | 8 |
NONE => PolyML.PrettyString "<future>" |
9 |
| 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
|
10 |
| SOME (Exn.Result y) => pretty (y, depth))); |
|
30633
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
11 |
|
| 31318 | 12 |
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => |
|
30633
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
13 |
(case Lazy.peek x of |
| 31318 | 14 |
NONE => PolyML.PrettyString "<lazy>" |
15 |
| 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
|
16 |
| SOME (Exn.Result y) => pretty (y, depth))); |
|
30633
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
17 |