# HG changeset patch
# User wenzelm
# Date 1222716404 -7200
# Node ID 419954d268863098a9b20ab86ecc15df19f2b344
# Parent  ee73353fb87ce3290b694667d007890b8120300a
install_pp Future.T (polyml only);

diff -r ee73353fb87c -r 419954d26886 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Mon Sep 29 21:26:41 2008 +0200
+++ b/src/Pure/pure_setup.ML	Mon Sep 29 21:26:44 2008 +0200
@@ -30,6 +30,13 @@
 
 install_pp (make_pp ["TaskQueue", "task"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_task));
 install_pp (make_pp ["TaskQueue", "group"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_group));
+
+if String.isPrefix "polyml" ml_system then
+  ML_Context.eval false Position.none
+    "install_pp ((make_pp [\"Future\", \"T\"] (Pretty.pprint o Pretty.str o Future.str_of)):\
+    \  ('a, 'a Future.T) pp)"
+else ();
+
 install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.enum "," "{" "}" o
   map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
 install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);