src/Pure/ML/install_pp_polyml.ML
author wenzelm
Wed, 11 Aug 2010 13:39:36 +0200
changeset 38327 d6afb77b0f6d
parent 31314 src/Pure/ML-Systems/install_pp_polyml.ML@b58d6a33b57f
child 43761 e72ba84ae58f
permissions -rw-r--r--
more precise and more maintainable dependencies;

(*  Title:      Pure/ML/install_pp_polyml.ML
    Author:     Makarius

Extra toplevel pretty-printing for Poly/ML.
*)

PolyML.install_pp
  (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
    (case Future.peek x of
      NONE => str "<future>"
    | SOME (Exn.Exn _) => str "<failed>"
    | SOME (Exn.Result y) => print (y, depth)));

PolyML.install_pp
  (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
    (case Lazy.peek x of
      NONE => str "<lazy>"
    | SOME (Exn.Exn _) => str "<failed>"
    | SOME (Exn.Result y) => print (y, depth)));