src/Pure/ML/install_pp_polyml-5.3.ML
author wenzelm
Wed Dec 29 20:41:33 2010 +0100 (2010-12-29)
changeset 41415 23533273220a
parent 38327 d6afb77b0f6d
child 43761 e72ba84ae58f
permissions -rw-r--r--
tuned ML toplevel pp for type string: observe depth limit;
     1 (*  Title:      Pure/ML/install_pp_polyml-5.3.ML
     2     Author:     Makarius
     3 
     4 Extra toplevel pretty-printing for Poly/ML 5.3.0.
     5 *)
     6 
     7 PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
     8   ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
     9 
    10 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
    11   pretty (Synchronized.value var, depth));
    12 
    13 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
    14   (case Future.peek x of
    15     NONE => PolyML.PrettyString "<future>"
    16   | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
    17   | SOME (Exn.Result y) => pretty (y, depth)));
    18 
    19 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
    20   (case Lazy.peek x of
    21     NONE => PolyML.PrettyString "<lazy>"
    22   | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
    23   | SOME (Exn.Result y) => pretty (y, depth)));
    24 
    25 PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
    26   let
    27     open PolyML;
    28     val from_ML = Pretty.from_ML o pretty_ml;
    29     fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
    30     fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
    31     fun prt_term parens dp (t as _ $ _) =
    32           op :: (strip_comb t)
    33           |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
    34           |> Pretty.separate " $"
    35           |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
    36       | prt_term _ dp (Abs (x, T, body)) =
    37           prt_apps "Abs"
    38            [from_ML (prettyRepresentation (x, dp - 1)),
    39             from_ML (prettyRepresentation (T, dp - 2)),
    40             prt_term false (dp - 3) body]
    41       | prt_term _ dp (Const const) =
    42           prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1)))
    43       | prt_term _ dp (Free free) =
    44           prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1)))
    45       | prt_term _ dp (Var var) =
    46           prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1)))
    47       | prt_term _ dp (Bound i) =
    48           prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1)));
    49   in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end);
    50