equal
deleted
inserted
replaced
|
1 (* Title: Pure/ML-Systems/install_pp_polyml-5.3.ML |
|
2 |
|
3 Extra toplevel pretty-printing for Poly/ML 5.3. |
|
4 *) |
|
5 |
|
6 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => |
|
7 (case Future.peek x of |
|
8 NONE => PolyML.PrettyString "<future>" |
|
9 | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" |
|
10 | SOME (Exn.Result y) => pretty (y, depth))); |
|
11 |
|
12 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => |
|
13 (case Lazy.peek x of |
|
14 NONE => PolyML.PrettyString "<lazy>" |
|
15 | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" |
|
16 | SOME (Exn.Result y) => pretty (y, depth))); |
|
17 |