src/Pure/Concurrent/lazy.ML
changeset 62819 d3ff367a16a0
parent 62663 bea354f6ff21
child 62823 751bcf0473a7
equal deleted inserted replaced
62818:2733b240bfea 62819:d3ff367a16a0
   101 
   101 
   102 
   102 
   103 (* toplevel pretty printing *)
   103 (* toplevel pretty printing *)
   104 
   104 
   105 val _ =
   105 val _ =
   106   PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
   106   ML_system_pp (fn depth => fn pretty => fn x =>
   107     (case peek x of
   107     (case peek x of
   108       NONE => PolyML.PrettyString "<lazy>"
   108       NONE => PolyML.PrettyString "<lazy>"
   109     | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
   109     | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
   110     | SOME (Exn.Res y) => pretty (y, depth)));
   110     | SOME (Exn.Res y) => pretty (y, depth)));
   111 
   111