src/Pure/ML/install_pp_polyml.ML
changeset 38327 d6afb77b0f6d
parent 31314 b58d6a33b57f
child 43761 e72ba84ae58f
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/install_pp_polyml.ML	Wed Aug 11 13:39:36 2010 +0200
@@ -0,0 +1,20 @@
+(*  Title:      Pure/ML/install_pp_polyml.ML
+    Author:     Makarius
+
+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)));
+