src/Pure/ML-Systems/install_pp_polyml-5.3.ML
author wenzelm
Thu Oct 01 23:27:05 2009 +0200 (2009-10-01)
changeset 32843 c8f5a7c8353f
parent 31433 12f5f6af3d2d
child 33538 edf497b5b5d2
permissions -rw-r--r--
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
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