src/Pure/ML-Systems/install_pp_polyml-5.3.ML
author wenzelm
Mon, 09 Nov 2009 21:30:54 +0100
changeset 33538 edf497b5b5d2
parent 31433 12f5f6af3d2d
child 33545 d8903f0002e5
permissions -rw-r--r--
setup for official Poly/ML 5.3.0, which is now the default;
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
33538
edf497b5b5d2 setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents: 31433
diff changeset
     3
Extra toplevel pretty-printing for Poly/ML 5.3.0.
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