src/Pure/Concurrent/lazy.ML
changeset 62823 751bcf0473a7
parent 62819 d3ff367a16a0
child 62891 7a11ea5c9626
equal deleted inserted replaced
62822:941b6a48ff67 62823:751bcf0473a7
   103 (* toplevel pretty printing *)
   103 (* toplevel pretty printing *)
   104 
   104 
   105 val _ =
   105 val _ =
   106   ML_system_pp (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_Pretty.PrettyString "<lazy>"
   109     | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
   109     | SOME (Exn.Exn _) => PolyML_Pretty.PrettyString "<failed>"
   110     | SOME (Exn.Res y) => pretty (y, depth)));
   110     | SOME (Exn.Res y) => pretty (y, depth)));
   111 
   111 
   112 end;
   112 end;
   113 
   113 
   114 type 'a lazy = 'a Lazy.lazy;
   114 type 'a lazy = 'a Lazy.lazy;