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