src/Pure/ML-Systems/install_pp_polyml-experimental.ML
author wenzelm
Tue, 24 Mar 2009 23:43:58 +0100
changeset 30714 88bc86d7dec3
parent 30633 cc18ae3c1c7f
child 31311 b82e55f51dcc
permissions -rw-r--r--
simplified addPrettyPrinter setup: may pass (fn ...) directly if type constraints are omitted -- addPrettyPrinter treated as a special case internally;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/install_pp_polyml-experimental.ML
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     2
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     3
Extra toplevel pretty-printing for Poly/ML; experimental version for
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     4
Poly/ML 5.3.
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     5
*)
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     6
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
     7
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
     8
  (case Future.peek x of
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     9
    NONE => PrettyString "<future>"
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
    10
  | SOME (Exn.Exn _) => 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
    11
  | 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
    12
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
    13
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
    14
  (case Lazy.peek x of
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
    15
    NONE => PrettyString "<lazy>"
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
    16
  | SOME (Exn.Exn _) => 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
    17
  | 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
    18