1.1 --- a/src/Pure/IsaMakefile	Thu Oct 09 21:06:08 2008 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Thu Oct 09 21:34:05 2008 +0200
     1.3 @@ -49,13 +49,13 @@
     1.4    Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML			\
     1.5    Isar/specification.ML Isar/subclass.ML Isar/theory_target.ML		\
     1.6    Isar/toplevel.ML ML-Systems/alice.ML ML-Systems/exn.ML		\
     1.7 -  ML-Systems/ml_name_space.ML ML-Systems/multithreading.ML		\
     1.8 -  ML-Systems/mosml.ML ML-Systems/multithreading_polyml.ML		\
     1.9 -  ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML		\
    1.10 -  ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-4.2.0.ML			\
    1.11 -  ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML			\
    1.12 -  ML-Systems/polyml_common.ML ML-Systems/polyml.ML			\
    1.13 -  ML-Systems/polyml_old_compiler4.ML					\
    1.14 +  ML-Systems/install_pp_polyml.ML ML-Systems/ml_name_space.ML		\
    1.15 +  ML-Systems/multithreading.ML ML-Systems/mosml.ML			\
    1.16 +  ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML	\
    1.17 +  ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML			\
    1.18 +  ML-Systems/polyml-4.2.0.ML ML-Systems/polyml-5.0.ML			\
    1.19 +  ML-Systems/polyml-5.1.ML ML-Systems/polyml_common.ML			\
    1.20 +  ML-Systems/polyml.ML ML-Systems/polyml_old_compiler4.ML		\
    1.21    ML-Systems/polyml_old_compiler5.ML ML-Systems/proper_int.ML		\
    1.22    ML-Systems/smlnj.ML ML-Systems/system_shell.ML			\
    1.23    ML-Systems/time_limit.ML ML-Systems/thread_dummy.ML			\

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/ML-Systems/install_pp_polyml.ML	Thu Oct 09 21:34:05 2008 +0200
     2.3 @@ -0,0 +1,16 @@
     2.4 +(*  Title:      Pure/ML-Systems/install_pp_polyml.ML
     2.5 +    ID:         $Id$
     2.6 +
     2.7 +Extra toplevel pretty-printing for Poly/ML.
     2.8 +*)
     2.9 +
    2.10 +install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Future.T) =>
    2.11 +  (case Future.peek x of
    2.12 +    NONE => str "<future>"
    2.13 +  | SOME (Exn.Exn _) => str "<failed future>"
    2.14 +  | SOME (Exn.Result y) => print (y, depth)));
    2.15 +
    2.16 +install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Susp.T) =>
    2.17 +  (case Susp.peek x of
    2.18 +    NONE => str "<delayed>"
    2.19 +  | SOME y => print (y, depth)));

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

     4.1 --- a/src/Pure/pure_setup.ML	Thu Oct 09 21:06:08 2008 +0200
     4.2 +++ b/src/Pure/pure_setup.ML	Thu Oct 09 21:34:05 2008 +0200
     4.3 @@ -30,13 +30,6 @@
     4.4  
     4.5  install_pp (make_pp ["TaskQueue", "task"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_task));
     4.6  install_pp (make_pp ["TaskQueue", "group"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_group));
     4.7 -
     4.8 -if String.isPrefix "polyml" ml_system then
     4.9 -  ML_Context.eval false Position.none
    4.10 -    "install_pp ((make_pp [\"Future\", \"T\"] (Pretty.pprint o Pretty.str o Future.str_of)):\
    4.11 -    \  ('a, 'a Future.T) pp)"
    4.12 -else ();
    4.13 -
    4.14  install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.enum "," "{" "}" o
    4.15    map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
    4.16  install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
    4.17 @@ -50,6 +43,9 @@
    4.18  install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode));
    4.19  install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident));
    4.20  
    4.21 +if String.isPrefix "polyml" ml_system then use "ML-Systems/install_pp_polyml.ML"
    4.22 +else ();
    4.23 +
    4.24  
    4.25  (* misc *)
    4.26