src/Pure/ML-Systems/install_pp_polyml.ML
author haftmann
Thu Oct 22 13:48:06 2009 +0200 (2009-10-22)
changeset 33063 4d462963a7db
parent 31314 b58d6a33b57f
permissions -rw-r--r--
map_range (and map_index) combinator
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@31314
     6
PolyML.install_pp
wenzelm@31314
     7
  (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
wenzelm@31314
     8
    (case Future.peek x of
wenzelm@31314
     9
      NONE => str "<future>"
wenzelm@31314
    10
    | SOME (Exn.Exn _) => str "<failed>"
wenzelm@31314
    11
    | SOME (Exn.Result y) => print (y, depth)));
wenzelm@28557
    12
wenzelm@31314
    13
PolyML.install_pp
wenzelm@31314
    14
  (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
wenzelm@31314
    15
    (case Lazy.peek x of
wenzelm@31314
    16
      NONE => str "<lazy>"
wenzelm@31314
    17
    | SOME (Exn.Exn _) => str "<failed>"
wenzelm@31314
    18
    | SOME (Exn.Result y) => print (y, depth)));
wenzelm@28672
    19