equal
deleted
inserted
replaced
1 (* Title: Pure/ML-Systems/install_pp_polyml-5.3.ML |
1 (* Title: Pure/ML-Systems/install_pp_polyml-5.3.ML |
2 |
2 |
3 Extra toplevel pretty-printing for Poly/ML 5.3. |
3 Extra toplevel pretty-printing for Poly/ML 5.3.0. |
4 *) |
4 *) |
5 |
5 |
6 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => |
6 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => |
7 (case Future.peek x of |
7 (case Future.peek x of |
8 NONE => PolyML.PrettyString "<future>" |
8 NONE => PolyML.PrettyString "<future>" |