# HG changeset patch
# User wenzelm
# Date 1498137632 -7200
# Node ID 1bd268ab885cd8d2dce9c90556e8a9265ee26208
# Parent  c88d1c36c9c3b706f20f71b0d50638208d291313
more informative task_statistics;

diff -r c88d1c36c9c3 -r 1bd268ab885c src/Pure/Concurrent/cache.ML
--- a/src/Pure/Concurrent/cache.ML	Thu Jun 22 14:27:13 2017 +0200
+++ b/src/Pure/Concurrent/cache.ML	Thu Jun 22 15:20:32 2017 +0200
@@ -23,7 +23,7 @@
           (case lookup tab x of
             SOME y => (y, tab)
           | NONE =>
-              let val y = Lazy.lazy (fn () => f x)
+              let val y = Lazy.lazy_name "cache" (fn () => f x)
               in (y, update (x, y) tab) end))
       |> Lazy.force;
   in apply end;
diff -r c88d1c36c9c3 -r 1bd268ab885c 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 *)
diff -r c88d1c36c9c3 -r 1bd268ab885c src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Jun 22 14:27:13 2017 +0200
+++ b/src/Pure/Isar/code.ML	Thu Jun 22 15:20:32 2017 +0200
@@ -142,7 +142,7 @@
         "\nof constant " ^ quote c ^
         "\nis too specific compared to declared type\n" ^
         string_of_typ thy ty_decl)
-  end; 
+  end;
 
 fun check_const thy = check_unoverload thy o check_bare_const thy;
 
@@ -411,7 +411,7 @@
 fun get_abstype_spec thy tyco = case get_type_entry thy tyco
  of SOME (vs, Abstractor spec) => (vs, spec)
   | _ => error ("Not an abstract type: " ^ tyco);
- 
+
 fun get_type_of_constr_or_abstr thy c =
   case (body_type o const_typ thy) c
    of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco
@@ -463,7 +463,7 @@
       ^ "\nof constant " ^ quote c
       ^ "\nis too specific compared to declared type\n"
       ^ string_of_typ thy ty_decl)
-  end; 
+  end;
 
 fun check_eqn thy { allow_nonlinear, allow_consts, allow_pats } thm (lhs, rhs) =
   let
@@ -760,7 +760,7 @@
 fun nothing_cert ctxt c = Nothing (dummy_thm ctxt c);
 
 fun cert_of_eqns ctxt c [] = Equations (dummy_thm ctxt c, [])
-  | cert_of_eqns ctxt c raw_eqns = 
+  | cert_of_eqns ctxt c raw_eqns =
       let
         val thy = Proof_Context.theory_of ctxt;
         val eqns = burrow_fst (canonize_thms thy) raw_eqns;
@@ -1104,7 +1104,7 @@
   let
     val thm = Thm.close_derivation raw_thm;
     val c = const_eqn thy thm;
-    fun update_subsume verbose (thm, proper) eqns = 
+    fun update_subsume verbose (thm, proper) eqns =
       let
         val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
           o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
@@ -1118,13 +1118,13 @@
             else false
           end;
         fun drop (thm', proper') = if (proper orelse not proper')
-          andalso matches_args (args_of thm') then 
+          andalso matches_args (args_of thm') then
             (if verbose then warning ("Code generator: dropping subsumed code equation\n" ^
                 Thm.string_of_thm_global thy thm') else (); true)
           else false;
       in (thm, proper) :: filter_out drop eqns end;
     fun natural_order eqns =
-      (eqns, Lazy.lazy (fn () => fold (update_subsume false) eqns []))
+      (eqns, Lazy.lazy_name "code" (fn () => fold (update_subsume false) eqns []))
     fun add_eqn' true Unimplemented = Eqns_Default (natural_order [(thm, proper)])
       | add_eqn' true (Eqns_Default (eqns, _)) = Eqns_Default (natural_order ((thm, proper) :: eqns))
           (*this restores the natural order and drops syntactic redundancies*)
diff -r c88d1c36c9c3 -r 1bd268ab885c src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Jun 22 14:27:13 2017 +0200
+++ b/src/Pure/PIDE/command.ML	Thu Jun 22 15:20:32 2017 +0200
@@ -264,7 +264,7 @@
             (fn () =>
               read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) ();
       in eval_state keywords span tr eval_state0 end;
-  in Eval {exec_id = exec_id, eval_process = Lazy.lazy process} end;
+  in Eval {exec_id = exec_id, eval_process = Lazy.lazy_name "Command.eval" process} end;
 
 end;
 
@@ -322,7 +322,7 @@
       in
         Print {
           name = name, args = args, delay = delay, pri = pri, persistent = persistent,
-          exec_id = exec_id, print_process = Lazy.lazy process}
+          exec_id = exec_id, print_process = Lazy.lazy_name "Command.print" process}
       end;
 
     fun bad_print name args exn =
diff -r c88d1c36c9c3 -r 1bd268ab885c src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Jun 22 14:27:13 2017 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Jun 22 15:20:32 2017 +0200
@@ -371,7 +371,7 @@
     let
       val id = Document_ID.print command_id;
       val span =
-        Lazy.lazy (fn () =>
+        Lazy.lazy_name "Document.define_command" (fn () =>
           Position.setmp_thread_data (Position.id_only id)
             (fn () =>
               let
diff -r c88d1c36c9c3 -r 1bd268ab885c src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Jun 22 14:27:13 2017 +0200
+++ b/src/Pure/Syntax/syntax.ML	Thu Jun 22 15:20:32 2017 +0200
@@ -540,7 +540,7 @@
           else
             let
               val input' = new_xprods2 @ input1;
-              val gram' = Lazy.lazy (fn () => Parser.make_gram input');
+              val gram' = Lazy.lazy_name "Syntax.merge_syntax" (fn () => Parser.make_gram input');
             in (input', gram') end);
   in
     Syntax
diff -r c88d1c36c9c3 -r 1bd268ab885c src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Jun 22 14:27:13 2017 +0200
+++ b/src/Pure/proofterm.ML	Thu Jun 22 15:20:32 2017 +0200
@@ -203,7 +203,7 @@
 fun make_thm_node name prop body =
   Thm_Node {name = name, prop = prop, body = body,
     consolidate =
-      Lazy.lazy (fn () =>
+      Lazy.lazy_name "Proofterm.make_thm_node" (fn () =>
         let val PBody {thms, ...} = Future.join body
         in List.app consolidate (join_thms thms) end)};