equal
deleted
inserted
replaced
103 (* toplevel pretty printing *) |
103 (* toplevel pretty printing *) |
104 |
104 |
105 val _ = |
105 val _ = |
106 ML_system_pp (fn depth => fn pretty => fn x => |
106 ML_system_pp (fn depth => fn pretty => fn x => |
107 (case peek x of |
107 (case peek x of |
108 NONE => PolyML.PrettyString "<lazy>" |
108 NONE => PolyML_Pretty.PrettyString "<lazy>" |
109 | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" |
109 | SOME (Exn.Exn _) => PolyML_Pretty.PrettyString "<failed>" |
110 | SOME (Exn.Res y) => pretty (y, depth))); |
110 | SOME (Exn.Res y) => pretty (y, depth))); |
111 |
111 |
112 end; |
112 end; |
113 |
113 |
114 type 'a lazy = 'a Lazy.lazy; |
114 type 'a lazy = 'a Lazy.lazy; |