src/Pure/ML-Systems/install_pp_polyml.ML
author wenzelm
Sun, 31 May 2009 14:51:21 +0200
changeset 31312 1c00e4ff3c99
parent 29564 f8b933a62151
child 31314 b58d6a33b57f
permissions -rw-r--r--
more modular setup of runtime compilation;

(*  Title:      Pure/ML-Systems/install_pp_polyml.ML

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

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)));

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)));