# HG changeset patch
# User wenzelm
# Date 1258647988 -3600
# Node ID f962c761a38f598d73e45bf049c742a85b3a0911
# Parent  c679f05600cd471056469080555fec274f13609a
toplevel pretty printer for Synchronized.var;

diff -r c679f05600cd -r f962c761a38f src/Pure/ML-Systems/install_pp_polyml-5.3.ML
--- a/src/Pure/ML-Systems/install_pp_polyml-5.3.ML	Thu Nov 19 14:46:33 2009 +0100
+++ b/src/Pure/ML-Systems/install_pp_polyml-5.3.ML	Thu Nov 19 17:26:28 2009 +0100
@@ -3,6 +3,9 @@
 Extra toplevel pretty-printing for Poly/ML 5.3.0.
 *)
 
+PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
+  pretty (Synchronized.value var, depth));
+
 PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
   (case Future.peek x of
     NONE => PolyML.PrettyString "<future>"