src/Pure/ML-Systems/install_pp_polyml-5.3.ML
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 31433 12f5f6af3d2d
child 33538 edf497b5b5d2
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
wenzelm@31433
     1
(*  Title:      Pure/ML-Systems/install_pp_polyml-5.3.ML
wenzelm@30633
     2
wenzelm@31433
     3
Extra toplevel pretty-printing for Poly/ML 5.3.
wenzelm@30633
     4
*)
wenzelm@30633
     5
wenzelm@31318
     6
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
wenzelm@30633
     7
  (case Future.peek x of
wenzelm@31318
     8
    NONE => PolyML.PrettyString "<future>"
wenzelm@31318
     9
  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
wenzelm@30714
    10
  | SOME (Exn.Result y) => pretty (y, depth)));
wenzelm@30633
    11
wenzelm@31318
    12
PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
wenzelm@30633
    13
  (case Lazy.peek x of
wenzelm@31318
    14
    NONE => PolyML.PrettyString "<lazy>"
wenzelm@31318
    15
  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
wenzelm@30714
    16
  | SOME (Exn.Result y) => pretty (y, depth)));
wenzelm@30633
    17