src/Pure/ML/install_pp_polyml.ML
changeset 47980 c81801f881b3
parent 43791 5e9a1d71f94d
child 47986 ca7104aebb74
equal deleted inserted replaced
47979:59ec72d3d0b9 47980:c81801f881b3
       
     1 (*  Title:      Pure/ML/install_pp_polyml.ML
       
     2     Author:     Makarius
       
     3 
       
     4 Extra toplevel pretty-printing for Poly/ML 5.3.0 or later.
       
     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 _ => fn tree =>
       
    11   ml_pretty (Pretty.to_ML (XML.pretty depth tree)));
       
    12 
       
    13 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
       
    14   pretty (Synchronized.value var, depth));
       
    15 
       
    16 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
       
    17   (case Future.peek x of
       
    18     NONE => PolyML.PrettyString "<future>"
       
    19   | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
       
    20   | SOME (Exn.Res y) => pretty (y, depth)));
       
    21 
       
    22 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
       
    23   (case Lazy.peek x of
       
    24     NONE => PolyML.PrettyString "<lazy>"
       
    25   | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
       
    26   | SOME (Exn.Res y) => pretty (y, depth)));
       
    27 
       
    28 PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
       
    29   let
       
    30     open PolyML;
       
    31     val from_ML = Pretty.from_ML o pretty_ml;
       
    32     fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
       
    33     fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
       
    34     fun prt_term parens dp (t as _ $ _) =
       
    35           op :: (strip_comb t)
       
    36           |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
       
    37           |> Pretty.separate " $"
       
    38           |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
       
    39       | prt_term _ dp (Abs (x, T, body)) =
       
    40           prt_apps "Abs"
       
    41            [from_ML (prettyRepresentation (x, dp - 1)),
       
    42             from_ML (prettyRepresentation (T, dp - 2)),
       
    43             prt_term false (dp - 3) body]
       
    44       | prt_term _ dp (Const const) =
       
    45           prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1)))
       
    46       | prt_term _ dp (Free free) =
       
    47           prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1)))
       
    48       | prt_term _ dp (Var var) =
       
    49           prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1)))
       
    50       | prt_term _ dp (Bound i) =
       
    51           prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1)));
       
    52   in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end);
       
    53