src/Pure/Concurrent/lazy.ML

--- a/src/Pure/Concurrent/lazy.ML	Thu Jun 22 14:27:13 2017 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Thu Jun 22 15:20:32 2017 +0200
@@ -9,6 +9,7 @@
 signature LAZY =
 sig
   type 'a lazy
+  val lazy_name: string -> (unit -> 'a) -> 'a lazy
   val lazy: (unit -> 'a) -> 'a lazy
   val value: 'a -> 'a lazy
   val peek: 'a lazy -> 'a Exn.result option
@@ -26,13 +27,14 @@
 (* datatype *)
 
 datatype 'a expr =
-  Expr of unit -> 'a |
+  Expr of string * (unit -> 'a) |
   Result of 'a future;
 
 abstype 'a lazy = Lazy of 'a expr Synchronized.var
 with
 
-fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
+fun lazy_name name e = Lazy (Synchronized.var "lazy" (Expr (name, e)));
+fun lazy e = lazy_name "lazy" e;
 fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
 
 fun peek (Lazy var) =
@@ -65,13 +67,13 @@
         let
           val (expr, x) =
             Synchronized.change_result var
-              (fn Expr e =>
-                    let val x = Future.promise_name "lazy" I
-                    in ((SOME e, x), Result x) end
+              (fn Expr (name, e) =>
+                    let val x = Future.promise_name name I
+                    in ((SOME (name, e), x), Result x) end
                 | Result x => ((NONE, x), Result x));
         in
           (case expr of
-            SOME e =>
+            SOME (name, e) =>
               let
                 val res0 = Exn.capture (restore_attributes e) ();
                 val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
@@ -80,7 +82,7 @@
                   interrupt, until there is a fresh start*)
                 val _ =
                   if Exn.is_interrupt_exn res then
-                    Synchronized.change var (fn _ => Expr e)
+                    Synchronized.change var (fn _ => Expr (name, e))
                   else ();
               in res end
           | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
@@ -90,7 +92,7 @@
 end;
 
 fun force r = Exn.release (force_result r);
-fun map f x = lazy (fn () => f (force x));
+fun map f x = lazy_name "Lazy.map" (fn () => f (force x));
 
 
 (* future evaluation *)