simplified addPrettyPrinter setup: may pass (fn ...) directly if type constraints are omitted -- addPrettyPrinter treated as a special case internally;
authorwenzelm
Tue, 24 Mar 2009 23:43:58 +0100
changeset 30714 88bc86d7dec3
parent 30713 b1a87e3971a3
child 30715 e23e15f52d42
child 30735 e925e4a7f237
child 30737 9ffd27558916
simplified addPrettyPrinter setup: may pass (fn ...) directly if type constraints are omitted -- addPrettyPrinter treated as a special case internally;
src/Pure/ML-Systems/install_pp_polyml-experimental.ML
--- a/src/Pure/ML-Systems/install_pp_polyml-experimental.ML	Tue Mar 24 22:56:17 2009 +0100
+++ b/src/Pure/ML-Systems/install_pp_polyml-experimental.ML	Tue Mar 24 23:43:58 2009 +0100
@@ -4,24 +4,15 @@
 Poly/ML 5.3.
 *)
 
-local
-
-fun pretty_future depth (pretty: 'a * int -> pretty) (x: 'a future) =
+addPrettyPrinter (fn depth => fn pretty => fn x =>
   (case Future.peek x of
     NONE => PrettyString "<future>"
   | SOME (Exn.Exn _) => PrettyString "<failed>"
-  | SOME (Exn.Result y) => pretty (y, depth));
+  | SOME (Exn.Result y) => pretty (y, depth)));
 
-fun pretty_lazy depth (pretty: 'a * int -> pretty) (x: 'a lazy) =
+addPrettyPrinter (fn depth => fn pretty => fn x =>
   (case Lazy.peek x of
     NONE => PrettyString "<lazy>"
   | SOME (Exn.Exn _) => PrettyString "<failed>"
-  | SOME (Exn.Result y) => pretty (y, depth));
-
-in
+  | SOME (Exn.Result y) => pretty (y, depth)));
 
-val _ = addPrettyPrinter pretty_future;
-val _ = addPrettyPrinter pretty_lazy;
-
-end;
-