src/Pure/ML/install_pp_polyml.ML
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 47986 ca7104aebb74
child 50910 54f06ba192ef
permissions -rw-r--r--
more official command specifications, including source position;
wenzelm@47980
     1
(*  Title:      Pure/ML/install_pp_polyml.ML
wenzelm@38327
     2
    Author:     Makarius
wenzelm@30633
     3
wenzelm@47980
     4
Extra toplevel pretty-printing for Poly/ML 5.3.0 or later.
wenzelm@30633
     5
*)
wenzelm@30633
     6
wenzelm@41415
     7
PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
wenzelm@41415
     8
  ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
wenzelm@41415
     9
wenzelm@43791
    10
PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
wenzelm@43791
    11
  ml_pretty (Pretty.to_ML (XML.pretty depth tree)));
wenzelm@43791
    12
wenzelm@33767
    13
PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
wenzelm@33767
    14
  pretty (Synchronized.value var, depth));
wenzelm@33767
    15
wenzelm@31318
    16
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
wenzelm@30633
    17
  (case Future.peek x of
wenzelm@31318
    18
    NONE => PolyML.PrettyString "<future>"
wenzelm@31318
    19
  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
wenzelm@43761
    20
  | SOME (Exn.Res y) => pretty (y, depth)));
wenzelm@30633
    21
wenzelm@31318
    22
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
wenzelm@30633
    23
  (case Lazy.peek x of
wenzelm@31318
    24
    NONE => PolyML.PrettyString "<lazy>"
wenzelm@31318
    25
  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
wenzelm@43761
    26
  | SOME (Exn.Res y) => pretty (y, depth)));
wenzelm@30633
    27
wenzelm@33545
    28
PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
wenzelm@33545
    29
  let
wenzelm@33545
    30
    open PolyML;
wenzelm@33545
    31
    val from_ML = Pretty.from_ML o pretty_ml;
wenzelm@33545
    32
    fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
wenzelm@33545
    33
    fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
wenzelm@33545
    34
    fun prt_term parens dp (t as _ $ _) =
wenzelm@33545
    35
          op :: (strip_comb t)
wenzelm@33545
    36
          |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
wenzelm@33545
    37
          |> Pretty.separate " $"
wenzelm@33545
    38
          |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
wenzelm@33545
    39
      | prt_term _ dp (Abs (x, T, body)) =
wenzelm@33545
    40
          prt_apps "Abs"
wenzelm@33545
    41
           [from_ML (prettyRepresentation (x, dp - 1)),
wenzelm@33545
    42
            from_ML (prettyRepresentation (T, dp - 2)),
wenzelm@33545
    43
            prt_term false (dp - 3) body]
wenzelm@33545
    44
      | prt_term _ dp (Const const) =
wenzelm@33545
    45
          prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1)))
wenzelm@33545
    46
      | prt_term _ dp (Free free) =
wenzelm@33545
    47
          prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1)))
wenzelm@33545
    48
      | prt_term _ dp (Var var) =
wenzelm@33545
    49
          prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1)))
wenzelm@33545
    50
      | prt_term _ dp (Bound i) =
wenzelm@33545
    51
          prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1)));
wenzelm@33545
    52
  in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end);
wenzelm@33545
    53