| author | hoelzl |
| Wed, 29 Apr 2009 20:19:50 +0200 | |
| changeset 31098 | 73dd67adf90a |
| parent 30714 | 88bc86d7dec3 |
| child 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 |
|
|
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
3 |
Extra toplevel pretty-printing for Poly/ML; experimental version for |
|
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
4 |
Poly/ML 5.3. |
|
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
5 |
*) |
|
cc18ae3c1c7f
extra toplevel pretty-printing 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 pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
8 |
(case Future.peek x of |
|
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
9 |
NONE => PrettyString "<future>" |
|
cc18ae3c1c7f
extra toplevel pretty-printing 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 pretty-printing 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 pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
14 |
(case Lazy.peek x of |
|
cc18ae3c1c7f
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
15 |
NONE => PrettyString "<lazy>" |
|
cc18ae3c1c7f
extra toplevel pretty-printing 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 pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset
|
18 |