author | wenzelm |
Sun, 31 May 2009 14:46:44 +0200 | |
changeset 31311 | b82e55f51dcc |
parent 30714 | 88bc86d7dec3 |
child 31318 | 133d1cfd6ae7 |
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 |
|
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 pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
7 |
(case Future.peek x of |
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
8 |
NONE => PrettyString "<future>" |
cc18ae3c1c7f
extra toplevel pretty-printing 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 pretty-printing 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 pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
13 |
(case Lazy.peek x of |
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
14 |
NONE => PrettyString "<lazy>" |
cc18ae3c1c7f
extra toplevel pretty-printing 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 pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
17 |