src/Pure/ML-Systems/install_pp_polyml-5.3.ML
changeset 33538 edf497b5b5d2
parent 31433 12f5f6af3d2d
child 33545 d8903f0002e5
equal deleted inserted replaced
33537:06c87d2c5b5a 33538:edf497b5b5d2
     1 (*  Title:      Pure/ML-Systems/install_pp_polyml-5.3.ML
     1 (*  Title:      Pure/ML-Systems/install_pp_polyml-5.3.ML
     2 
     2 
     3 Extra toplevel pretty-printing for Poly/ML 5.3.
     3 Extra toplevel pretty-printing for Poly/ML 5.3.0.
     4 *)
     4 *)
     5 
     5 
     6 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
     6 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
     7   (case Future.peek x of
     7   (case Future.peek x of
     8     NONE => PolyML.PrettyString "<future>"
     8     NONE => PolyML.PrettyString "<future>"