src/Pure/ML-Systems/install_pp_polyml.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29564 f8b933a62151
child 31314 b58d6a33b57f
permissions -rw-r--r--
use long names for old-style fold combinators;
wenzelm@28557
     1
(*  Title:      Pure/ML-Systems/install_pp_polyml.ML
wenzelm@28557
     2
wenzelm@28557
     3
Extra toplevel pretty-printing for Poly/ML.
wenzelm@28557
     4
*)
wenzelm@28557
     5
wenzelm@28975
     6
install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
wenzelm@28557
     7
  (case Future.peek x of
wenzelm@28557
     8
    NONE => str "<future>"
wenzelm@28570
     9
  | SOME (Exn.Exn _) => str "<failed>"
wenzelm@28557
    10
  | SOME (Exn.Result y) => print (y, depth)));
wenzelm@28557
    11
wenzelm@28975
    12
install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
wenzelm@28673
    13
  (case Lazy.peek x of
wenzelm@28673
    14
    NONE => str "<lazy>"
wenzelm@28672
    15
  | SOME (Exn.Exn _) => str "<failed>"
wenzelm@28672
    16
  | SOME (Exn.Result y) => print (y, depth)));
wenzelm@28672
    17