src/Pure/ML/install_pp_polyml.ML
author wenzelm
Thu, 24 May 2012 15:54:38 +0200
changeset 47986 ca7104aebb74
parent 43761 e72ba84ae58f
parent 47980 c81801f881b3
child 50910 54f06ba192ef
permissions -rw-r--r--
merged
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47980
c81801f881b3 simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents: 43791
diff changeset
     1
(*  Title:      Pure/ML/install_pp_polyml.ML
38327
d6afb77b0f6d more precise and more maintainable dependencies;
wenzelm
parents: 33767
diff changeset
     2
    Author:     Makarius
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
     3
47980
c81801f881b3 simplified Poly/ML setup -- 5.3.0 is now the common base-line;
wenzelm
parents: 43791
diff changeset
     4
Extra toplevel pretty-printing for Poly/ML 5.3.0 or later.
30633
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
41415
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 38327
diff changeset
     7
PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 38327
diff changeset
     8
  ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 38327
diff changeset
     9
43791
5e9a1d71f94d XML.pretty with depth limit;
wenzelm
parents: 43761
diff changeset
    10
PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
5e9a1d71f94d XML.pretty with depth limit;
wenzelm
parents: 43761
diff changeset
    11
  ml_pretty (Pretty.to_ML (XML.pretty depth tree)));
5e9a1d71f94d XML.pretty with depth limit;
wenzelm
parents: 43761
diff changeset
    12
33767
f962c761a38f toplevel pretty printer for Synchronized.var;
wenzelm
parents: 33545
diff changeset
    13
PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
f962c761a38f toplevel pretty printer for Synchronized.var;
wenzelm
parents: 33545
diff changeset
    14
  pretty (Synchronized.value var, depth));
f962c761a38f toplevel pretty printer for Synchronized.var;
wenzelm
parents: 33545
diff changeset
    15
31318
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    16
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
    17
  (case Future.peek x of
31318
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    18
    NONE => PolyML.PrettyString "<future>"
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    19
  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 41415
diff changeset
    20
  | SOME (Exn.Res y) => pretty (y, depth)));
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
    21
31318
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    22
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
    23
  (case Lazy.peek x of
31318
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    24
    NONE => PolyML.PrettyString "<lazy>"
133d1cfd6ae7 explicit PolyML qualification;
wenzelm
parents: 31311
diff changeset
    25
  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
43761
e72ba84ae58f tuned signature -- corresponding to Scala version;
wenzelm
parents: 41415
diff changeset
    26
  | SOME (Exn.Res y) => pretty (y, depth)));
30633
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff changeset
    27
33545
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    28
PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    29
  let
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    30
    open PolyML;
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    31
    val from_ML = Pretty.from_ML o pretty_ml;
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    32
    fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    33
    fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    34
    fun prt_term parens dp (t as _ $ _) =
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    35
          op :: (strip_comb t)
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    36
          |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    37
          |> Pretty.separate " $"
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    38
          |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    39
      | prt_term _ dp (Abs (x, T, body)) =
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    40
          prt_apps "Abs"
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    41
           [from_ML (prettyRepresentation (x, dp - 1)),
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    42
            from_ML (prettyRepresentation (T, dp - 2)),
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    43
            prt_term false (dp - 3) body]
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    44
      | prt_term _ dp (Const const) =
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    45
          prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1)))
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    46
      | prt_term _ dp (Free free) =
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    47
          prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1)))
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    48
      | prt_term _ dp (Var var) =
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    49
          prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1)))
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    50
      | prt_term _ dp (Bound i) =
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    51
          prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1)));
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    52
  in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end);
d8903f0002e5 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm
parents: 33538
diff changeset
    53