equal
deleted
inserted
replaced
|
1 (* Title: Pure/ML-Systems/install_pp_polyml-experimental.ML |
|
2 |
|
3 Extra toplevel pretty-printing for Poly/ML; experimental version for |
|
4 Poly/ML 5.3. |
|
5 *) |
|
6 |
|
7 local |
|
8 |
|
9 fun pretty_future depth (pretty: 'a * int -> pretty) (x: 'a future) = |
|
10 (case Future.peek x of |
|
11 NONE => PrettyString "<future>" |
|
12 | SOME (Exn.Exn _) => PrettyString "<failed>" |
|
13 | SOME (Exn.Result y) => pretty (y, depth)); |
|
14 |
|
15 fun pretty_lazy depth (pretty: 'a * int -> pretty) (x: 'a lazy) = |
|
16 (case Lazy.peek x of |
|
17 NONE => PrettyString "<lazy>" |
|
18 | SOME (Exn.Exn _) => PrettyString "<failed>" |
|
19 | SOME (Exn.Result y) => pretty (y, depth)); |
|
20 |
|
21 in |
|
22 |
|
23 val _ = addPrettyPrinter pretty_future; |
|
24 val _ = addPrettyPrinter pretty_lazy; |
|
25 |
|
26 end; |
|
27 |