src/Pure/ML-Systems/install_pp_polyml-experimental.ML
changeset 31311 b82e55f51dcc
parent 30714 88bc86d7dec3
child 31318 133d1cfd6ae7
equal deleted inserted replaced
31310:b5365a9db718 31311:b82e55f51dcc
     1 (*  Title:      Pure/ML-Systems/install_pp_polyml-experimental.ML
     1 (*  Title:      Pure/ML-Systems/install_pp_polyml-experimental.ML
     2 
     2 
     3 Extra toplevel pretty-printing for Poly/ML; experimental version for
     3 Extra toplevel pretty-printing for Poly/ML 5.3 (SVN experimental).
     4 Poly/ML 5.3.
       
     5 *)
     4 *)
     6 
     5 
     7 addPrettyPrinter (fn depth => fn pretty => fn x =>
     6 addPrettyPrinter (fn depth => fn pretty => fn x =>
     8   (case Future.peek x of
     7   (case Future.peek x of
     9     NONE => PrettyString "<future>"
     8     NONE => PrettyString "<future>"