src/Pure/ML-Systems/install_pp_polyml.ML
author wenzelm
Thu, 09 Oct 2008 21:34:05 +0200
changeset 28557 6a661aeff564
child 28570 81d97311c057
permissions -rw-r--r--
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28557
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/install_pp_polyml.ML
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff changeset
     3
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff changeset
     4
Extra toplevel pretty-printing for Poly/ML.
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff changeset
     5
*)
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff changeset
     6
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff changeset
     7
install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Future.T) =>
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff changeset
     8
  (case Future.peek x of
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff changeset
     9
    NONE => str "<future>"
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff changeset
    10
  | SOME (Exn.Exn _) => str "<failed future>"
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff changeset
    11
  | SOME (Exn.Result y) => print (y, depth)));
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff changeset
    12
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff changeset
    13
install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Susp.T) =>
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff changeset
    14
  (case Susp.peek x of
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff changeset
    15
    NONE => str "<delayed>"
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff changeset
    16
  | SOME y => print (y, depth)));