src/Pure/Concurrent/future.ML
changeset 62663 bea354f6ff21
parent 62505 9e2a65912111
child 62819 d3ff367a16a0
equal deleted inserted replaced
62662:291cc01f56f5 62663:bea354f6ff21
    97 fun result_of (Future {result, ...}) = result;
    97 fun result_of (Future {result, ...}) = result;
    98 
    98 
    99 fun peek x = Single_Assignment.peek (result_of x);
    99 fun peek x = Single_Assignment.peek (result_of x);
   100 fun is_finished x = is_some (peek x);
   100 fun is_finished x = is_some (peek x);
   101 
   101 
       
   102 val _ =
       
   103   PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
       
   104     (case peek x of
       
   105       NONE => PolyML.PrettyString "<future>"
       
   106     | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
       
   107     | SOME (Exn.Res y) => pretty (y, depth)));
       
   108 
   102 
   109 
   103 
   110 
   104 (** scheduling **)
   111 (** scheduling **)
   105 
   112 
   106 (* synchronization *)
   113 (* synchronization *)
   663 val map = map_future;
   670 val map = map_future;
   664 
   671 
   665 end;
   672 end;
   666 
   673 
   667 type 'a future = 'a Future.future;
   674 type 'a future = 'a Future.future;
   668