src/Pure/ML-Systems/install_pp_polyml.ML
changeset 38327 d6afb77b0f6d
parent 38326 01d2ef471ffe
child 38328 36afb56ec49e
child 38344 36f179131633
child 38345 8b8fc27c1872
--- a/src/Pure/ML-Systems/install_pp_polyml.ML	Wed Aug 11 12:50:33 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      Pure/ML-Systems/install_pp_polyml.ML
-
-Extra toplevel pretty-printing for Poly/ML.
-*)
-
-PolyML.install_pp
-  (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
-    (case Future.peek x of
-      NONE => str "<future>"
-    | SOME (Exn.Exn _) => str "<failed>"
-    | SOME (Exn.Result y) => print (y, depth)));
-
-PolyML.install_pp
-  (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
-    (case Lazy.peek x of
-      NONE => str "<lazy>"
-    | SOME (Exn.Exn _) => str "<failed>"
-    | SOME (Exn.Result y) => print (y, depth)));
-