author | wenzelm |
Sat, 13 Dec 2008 15:00:39 +0100 | |
changeset 29091 | b81fe045e799 |
parent 28975 | ec120dc11e8b |
child 29564 | f8b933a62151 |
permissions | -rw-r--r-- |
28557
6a661aeff564
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/install_pp_polyml.ML |
6a661aeff564
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
6a661aeff564
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff
changeset
|
3 |
|
6a661aeff564
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff
changeset
|
4 |
Extra toplevel pretty-printing for Poly/ML. |
6a661aeff564
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff
changeset
|
5 |
*) |
6a661aeff564
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff
changeset
|
6 |
|
28975 | 7 |
install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) => |
28557
6a661aeff564
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff
changeset
|
8 |
(case Future.peek x of |
6a661aeff564
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff
changeset
|
9 |
NONE => str "<future>" |
28570 | 10 |
| SOME (Exn.Exn _) => str "<failed>" |
28557
6a661aeff564
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff
changeset
|
11 |
| SOME (Exn.Result y) => print (y, depth))); |
6a661aeff564
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff
changeset
|
12 |
|
28975 | 13 |
install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) => |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28672
diff
changeset
|
14 |
(case Lazy.peek x of |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28672
diff
changeset
|
15 |
NONE => str "<lazy>" |
28672 | 16 |
| SOME (Exn.Exn _) => str "<failed>" |
17 |
| SOME (Exn.Result y) => print (y, depth))); |
|
18 |