equal
deleted
inserted
replaced
101 |
101 |
102 |
102 |
103 (* toplevel pretty printing *) |
103 (* toplevel pretty printing *) |
104 |
104 |
105 val _ = |
105 val _ = |
106 PolyML.addPrettyPrinter (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.PrettyString "<lazy>" |
109 | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" |
109 | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>" |
110 | SOME (Exn.Res y) => pretty (y, depth))); |
110 | SOME (Exn.Res y) => pretty (y, depth))); |
111 |
111 |