src/Pure/ML-Systems/install_pp_polyml-5.3.ML
author haftmann
Thu Oct 22 13:48:06 2009 +0200 (2009-10-22)
changeset 33063 4d462963a7db
parent 31433 12f5f6af3d2d
child 33538 edf497b5b5d2
permissions -rw-r--r--
map_range (and map_index) combinator
     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