src/Pure/ML-Systems/install_pp_polyml-5.3.ML
author wenzelm
Thu, 04 Jun 2009 19:15:54 +0200
changeset 31433 12f5f6af3d2d
parent 31318 src/Pure/ML-Systems/install_pp_polyml-experimental.ML@133d1cfd6ae7
child 33538 edf497b5b5d2
permissions -rw-r--r--
less experimental polyml-5.3;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31433
12f5f6af3d2d less experimental polyml-5.3;
wenzelm
parents: 31318
diff changeset
     1
(*  Title:      Pure/ML-Systems/install_pp_polyml-5.3.ML
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     2
31433
12f5f6af3d2d less experimental polyml-5.3;
wenzelm
parents: 31318
diff changeset
     3
Extra toplevel pretty-printing for Poly/ML 5.3.
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     4
*)
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     5
31318
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
     6
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     7
  (case Future.peek x of
31318
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
     8
    NONE => PolyML.PrettyString "<future>"
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
     9
  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
30714
88bc86d7dec3 simplified addPrettyPrinter setup: may pass (fn ...) directly if type constraints are omitted -- addPrettyPrinter treated as a special case internally;
wenzelm
parents: 30633
diff changeset
    10
  | SOME (Exn.Result y) => pretty (y, depth)));
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
    11
31318
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    12
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
    13
  (case Lazy.peek x of
31318
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    14
    NONE => PolyML.PrettyString "<lazy>"
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    15
  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
30714
88bc86d7dec3 simplified addPrettyPrinter setup: may pass (fn ...) directly if type constraints are omitted -- addPrettyPrinter treated as a special case internally;
wenzelm
parents: 30633
diff changeset
    16
  | SOME (Exn.Result y) => pretty (y, depth)));
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
    17