src/Pure/ML-Systems/install_pp_polyml-experimental.ML
changeset 30714 88bc86d7dec3
parent 30633 cc18ae3c1c7f
child 31311 b82e55f51dcc
equal deleted inserted replaced
30713:b1a87e3971a3 30714:88bc86d7dec3
     2 
     2 
     3 Extra toplevel pretty-printing for Poly/ML; experimental version for
     3 Extra toplevel pretty-printing for Poly/ML; experimental version for
     4 Poly/ML 5.3.
     4 Poly/ML 5.3.
     5 *)
     5 *)
     6 
     6 
     7 local
     7 addPrettyPrinter (fn depth => fn pretty => fn x =>
     8 
       
     9 fun pretty_future depth (pretty: 'a * int -> pretty) (x: 'a future) =
       
    10   (case Future.peek x of
     8   (case Future.peek x of
    11     NONE => PrettyString "<future>"
     9     NONE => PrettyString "<future>"
    12   | SOME (Exn.Exn _) => PrettyString "<failed>"
    10   | SOME (Exn.Exn _) => PrettyString "<failed>"
    13   | SOME (Exn.Result y) => pretty (y, depth));
    11   | SOME (Exn.Result y) => pretty (y, depth)));
    14 
    12 
    15 fun pretty_lazy depth (pretty: 'a * int -> pretty) (x: 'a lazy) =
    13 addPrettyPrinter (fn depth => fn pretty => fn x =>
    16   (case Lazy.peek x of
    14   (case Lazy.peek x of
    17     NONE => PrettyString "<lazy>"
    15     NONE => PrettyString "<lazy>"
    18   | SOME (Exn.Exn _) => PrettyString "<failed>"
    16   | SOME (Exn.Exn _) => PrettyString "<failed>"
    19   | SOME (Exn.Result y) => pretty (y, depth));
    17   | SOME (Exn.Result y) => pretty (y, depth)));
    20 
    18 
    21 in
       
    22 
       
    23 val _ = addPrettyPrinter pretty_future;
       
    24 val _ = addPrettyPrinter pretty_lazy;
       
    25 
       
    26 end;
       
    27