extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;

--- a/src/Pure/IsaMakefile	Thu Oct 09 21:06:08 2008 +0200
+++ b/src/Pure/IsaMakefile	Thu Oct 09 21:34:05 2008 +0200
@@ -49,13 +49,13 @@
   Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML			\
   Isar/specification.ML Isar/subclass.ML Isar/theory_target.ML		\
   Isar/toplevel.ML ML-Systems/alice.ML ML-Systems/exn.ML		\
-  ML-Systems/ml_name_space.ML ML-Systems/multithreading.ML		\
-  ML-Systems/mosml.ML ML-Systems/multithreading_polyml.ML		\
-  ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML		\
-  ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-4.2.0.ML			\
-  ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML			\
-  ML-Systems/polyml_common.ML ML-Systems/polyml.ML			\
-  ML-Systems/polyml_old_compiler4.ML					\
+  ML-Systems/install_pp_polyml.ML ML-Systems/ml_name_space.ML		\
+  ML-Systems/multithreading.ML ML-Systems/mosml.ML			\
+  ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML	\
+  ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML			\
+  ML-Systems/polyml-4.2.0.ML ML-Systems/polyml-5.0.ML			\
+  ML-Systems/polyml-5.1.ML ML-Systems/polyml_common.ML			\
+  ML-Systems/polyml.ML ML-Systems/polyml_old_compiler4.ML		\
   ML-Systems/polyml_old_compiler5.ML ML-Systems/proper_int.ML		\
   ML-Systems/smlnj.ML ML-Systems/system_shell.ML			\
   ML-Systems/time_limit.ML ML-Systems/thread_dummy.ML			\

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/install_pp_polyml.ML	Thu Oct 09 21:34:05 2008 +0200
@@ -0,0 +1,16 @@
+(*  Title:      Pure/ML-Systems/install_pp_polyml.ML
+    ID:         $Id$
+
+Extra toplevel pretty-printing for Poly/ML.
+*)
+
+install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Future.T) =>
+  (case Future.peek x of
+    NONE => str "<future>"
+  | SOME (Exn.Exn _) => str "<failed future>"
+  | SOME (Exn.Result y) => print (y, depth)));
+
+install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Susp.T) =>
+  (case Susp.peek x of
+    NONE => str "<delayed>"
+  | SOME y => print (y, depth)));

--- a/src/Pure/ML-Systems/polyml_common.ML	Thu Oct 09 21:06:08 2008 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Thu Oct 09 21:34:05 2008 +0200
@@ -75,10 +75,6 @@
 
 (* toplevel pretty printing (see also Pure/pure_setup.ML) *)
 
-type ('a, 'b) pp =
-  (string -> unit) * (int * bool -> unit) * (int * int -> unit) * (unit -> unit) ->
-    int -> ('a * int -> unit) -> 'b -> unit;
-
 fun make_pp _ pprint (str, blk, brk, en) _ _ obj =
   pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
     fn () => brk (99999, 0), en);

--- a/src/Pure/pure_setup.ML	Thu Oct 09 21:06:08 2008 +0200
+++ b/src/Pure/pure_setup.ML	Thu Oct 09 21:34:05 2008 +0200
@@ -30,13 +30,6 @@
 
 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);
@@ -50,6 +43,9 @@
 install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode));
 install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident));
 
+if String.isPrefix "polyml" ml_system then use "ML-Systems/install_pp_polyml.ML"
+else ();
+
 
 (* misc *)