author | blanchet |
Wed, 02 Jun 2010 15:18:48 +0200 | |
changeset 37321 | 9d7cfae95b30 |
parent 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 |
|
31314 | 6 |
PolyML.install_pp |
7 |
(fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) => |
|
8 |
(case Future.peek x of |
|
9 |
NONE => str "<future>" |
|
10 |
| SOME (Exn.Exn _) => str "<failed>" |
|
11 |
| SOME (Exn.Result y) => print (y, depth))); |
|
28557
6a661aeff564
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff
changeset
|
12 |
|
31314 | 13 |
PolyML.install_pp |
14 |
(fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) => |
|
15 |
(case Lazy.peek x of |
|
16 |
NONE => str "<lazy>" |
|
17 |
| SOME (Exn.Exn _) => str "<failed>" |
|
18 |
| SOME (Exn.Result y) => print (y, depth))); |
|
28672 | 19 |