author | wenzelm |
Sun, 01 Mar 2009 23:36:12 +0100 | |
changeset 30190 | 479806475f3c |
parent 29564 | f8b933a62151 |
child 31314 | b58d6a33b57f |
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 |
|
6a661aeff564
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff
changeset
|
3 |
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
|
4 |
*) |
6a661aeff564
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff
changeset
|
5 |
|
28975 | 6 |
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
|
7 |
(case Future.peek x of |
6a661aeff564
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff
changeset
|
8 |
NONE => str "<future>" |
28570 | 9 |
| SOME (Exn.Exn _) => str "<failed>" |
28557
6a661aeff564
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff
changeset
|
10 |
| 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
|
11 |
|
28975 | 12 |
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
|
13 |
(case Lazy.peek x of |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
28672
diff
changeset
|
14 |
NONE => str "<lazy>" |
28672 | 15 |
| SOME (Exn.Exn _) => str "<failed>" |
16 |
| SOME (Exn.Result y) => print (y, depth))); |
|
17 |