src/Pure/Concurrent/lazy.ML
changeset 62663 bea354f6ff21
parent 59348 8a6788917b32
child 62819 d3ff367a16a0
equal deleted inserted replaced
62662:291cc01f56f5 62663:bea354f6ff21
    97 
    97 
    98 fun future params x =
    98 fun future params x =
    99   if is_finished x then Future.value_result (force_result x)
    99   if is_finished x then Future.value_result (force_result x)
   100   else (singleton o Future.forks) params (fn () => force x);
   100   else (singleton o Future.forks) params (fn () => force x);
   101 
   101 
       
   102 
       
   103 (* toplevel pretty printing *)
       
   104 
       
   105 val _ =
       
   106   PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
       
   107     (case peek x of
       
   108       NONE => PolyML.PrettyString "<lazy>"
       
   109     | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
       
   110     | SOME (Exn.Res y) => pretty (y, depth)));
       
   111 
   102 end;
   112 end;
   103 
   113 
   104 type 'a lazy = 'a Lazy.lazy;
   114 type 'a lazy = 'a Lazy.lazy;
   105