src/Pure/ML/install_pp_polyml.ML
author wenzelm
Wed, 11 Aug 2010 13:39:36 +0200
changeset 38327 d6afb77b0f6d
parent 31314 src/Pure/ML-Systems/install_pp_polyml.ML@b58d6a33b57f
child 43761 e72ba84ae58f
permissions -rw-r--r--
more precise and more maintainable dependencies;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38327
d6afb77b0f6d more precise and more maintainable dependencies;
wenzelm
parents: 31314
diff changeset
     1
(*  Title:      Pure/ML/install_pp_polyml.ML
d6afb77b0f6d more precise and more maintainable dependencies;
wenzelm
parents: 31314
diff changeset
     2
    Author:     Makarius
28557
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
31314
b58d6a33b57f explicit PolyML.install_pp;
wenzelm
parents: 29564
diff changeset
     7
PolyML.install_pp
b58d6a33b57f explicit PolyML.install_pp;
wenzelm
parents: 29564
diff changeset
     8
  (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
b58d6a33b57f explicit PolyML.install_pp;
wenzelm
parents: 29564
diff changeset
     9
    (case Future.peek x of
b58d6a33b57f explicit PolyML.install_pp;
wenzelm
parents: 29564
diff changeset
    10
      NONE => str "<future>"
b58d6a33b57f explicit PolyML.install_pp;
wenzelm
parents: 29564
diff changeset
    11
    | SOME (Exn.Exn _) => str "<failed>"
b58d6a33b57f explicit PolyML.install_pp;
wenzelm
parents: 29564
diff changeset
    12
    | SOME (Exn.Result y) => print (y, depth)));
28557
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
wenzelm
parents:
diff changeset
    13
31314
b58d6a33b57f explicit PolyML.install_pp;
wenzelm
parents: 29564
diff changeset
    14
PolyML.install_pp
b58d6a33b57f explicit PolyML.install_pp;
wenzelm
parents: 29564
diff changeset
    15
  (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
b58d6a33b57f explicit PolyML.install_pp;
wenzelm
parents: 29564
diff changeset
    16
    (case Lazy.peek x of
b58d6a33b57f explicit PolyML.install_pp;
wenzelm
parents: 29564
diff changeset
    17
      NONE => str "<lazy>"
b58d6a33b57f explicit PolyML.install_pp;
wenzelm
parents: 29564
diff changeset
    18
    | SOME (Exn.Exn _) => str "<failed>"
b58d6a33b57f explicit PolyML.install_pp;
wenzelm
parents: 29564
diff changeset
    19
    | SOME (Exn.Result y) => print (y, depth)));
28672
0baf1d9c6780 adapted Susp.peek;
wenzelm
parents: 28570
diff changeset
    20