src/Pure/ML-Systems/install_pp_polyml-5.3.ML
changeset 31433 12f5f6af3d2d
parent 31318 133d1cfd6ae7
child 33538 edf497b5b5d2
equal deleted inserted replaced
31432:9858f32f9569 31433:12f5f6af3d2d
       
     1 (*  Title:      Pure/ML-Systems/install_pp_polyml-5.3.ML
       
     2 
       
     3 Extra toplevel pretty-printing for Poly/ML 5.3.
       
     4 *)
       
     5 
       
     6 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
       
     7   (case Future.peek x of
       
     8     NONE => PolyML.PrettyString "<future>"
       
     9   | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
       
    10   | SOME (Exn.Result y) => pretty (y, depth)));
       
    11 
       
    12 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
       
    13   (case Lazy.peek x of
       
    14     NONE => PolyML.PrettyString "<lazy>"
       
    15   | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
       
    16   | SOME (Exn.Result y) => pretty (y, depth)));
       
    17