# HG changeset patch
# User wenzelm
# Date 1498160937 -7200
# Node ID cad55bc7e37ddcaec63d5a75ef6edbc4a055ac93
# Parent  48cfbccaf3f459ac3782e37959a01a9106834e4e# Parent  8cfa8c7ee1f6c80dda2fd9fdbe7c1285bd7c6ed8
merged

diff -r 48cfbccaf3f4 -r cad55bc7e37d src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Jun 22 16:49:01 2017 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Jun 22 21:48:57 2017 +0200
@@ -959,7 +959,7 @@
     | SOME {vcs, path, ...} =>
         let
           val (proved, unproved) = partition_vcs vcs;
-          val _ = List.app Thm.consolidate (maps (#2 o snd) proved);
+          val _ = Thm.consolidate (maps (#2 o snd) proved);
           val (proved', proved'') =
             List.partition (fn (_, (_, thms, _, _)) =>
               exists (#oracle o Thm.peek_status) thms) proved;
diff -r 48cfbccaf3f4 -r cad55bc7e37d src/Pure/Concurrent/cache.ML
--- a/src/Pure/Concurrent/cache.ML	Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/Concurrent/cache.ML	Thu Jun 22 21:48:57 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 48cfbccaf3f4 -r cad55bc7e37d src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/Concurrent/event_timer.ML	Thu Jun 22 21:48:57 2017 +0200
@@ -148,7 +148,7 @@
   let
     val req: request Single_Assignment.var = Single_Assignment.var "request";
     fun abort () = ignore (cancel (Single_Assignment.await req));
-    val promise: unit future = Future.promise abort;
+    val promise: unit future = Future.promise_name "event_timer" abort;
     val _ = Single_Assignment.assign req (request time (Future.fulfill promise));
   in promise end);
 
diff -r 48cfbccaf3f4 -r cad55bc7e37d src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/Concurrent/future.ML	Thu Jun 22 21:48:57 2017 +0200
@@ -37,7 +37,7 @@
   val value: 'a -> 'a future
   val cond_forks: params -> (unit -> 'a) list -> 'a future list
   val map: ('a -> 'b) -> 'a future -> 'b future
-  val promise_group: group -> (unit -> unit) -> 'a future
+  val promise_name: string -> (unit -> unit) -> 'a future
   val promise: (unit -> unit) -> 'a future
   val fulfill_result: 'a future -> 'a Exn.result -> unit
   val fulfill: 'a future -> 'a -> unit
@@ -599,8 +599,9 @@
 
 (* promised futures -- fulfilled by external means *)
 
-fun promise_group group abort : 'a future =
+fun promise_name name abort : 'a future =
   let
+    val group = worker_subgroup ();
     val result = Single_Assignment.var "promise" : 'a result;
     fun assign () = assign_result group result Exn.interrupt_exn
       handle Fail _ => true
@@ -612,10 +613,10 @@
       Thread_Attributes.with_attributes Thread_Attributes.no_interrupts
         (fn _ => Exn.release (Exn.capture assign () before abort ()));
     val task = SYNCHRONIZED "enqueue_passive" (fn () =>
-      Unsynchronized.change_result queue (Task_Queue.enqueue_passive group job));
+      Unsynchronized.change_result queue (Task_Queue.enqueue_passive group name job));
   in Future {promised = true, task = task, result = result} end;
 
-fun promise abort = promise_group (worker_subgroup ()) abort;
+fun promise abort = promise_name "passive" abort;
 
 fun fulfill_result (Future {promised, task, result}) res =
   if not promised then raise Fail "Not a promised future"
diff -r 48cfbccaf3f4 -r cad55bc7e37d src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/Concurrent/lazy.ML	Thu Jun 22 21:48:57 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
@@ -16,6 +17,7 @@
   val is_finished: 'a lazy -> bool
   val force_result: 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
+  val force_list: 'a lazy list -> 'a list
   val map: ('a -> 'b) -> 'a lazy -> 'b lazy
   val future: Future.params -> 'a lazy -> 'a future
 end;
@@ -26,13 +28,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) =
@@ -40,6 +43,12 @@
     Expr _ => NONE
   | Result res => Future.peek res);
 
+fun pending (Lazy var) =
+  (case Synchronized.value var of
+    Expr _ => true
+  | Result _ => false);
+
+
 
 (* status *)
 
@@ -65,13 +74,13 @@
         let
           val (expr, x) =
             Synchronized.change_result var
-              (fn Expr e =>
-                    let val x = Future.promise 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 +89,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)) ())
@@ -89,8 +98,13 @@
 
 end;
 
-fun force r = Exn.release (force_result r);
-fun map f x = lazy (fn () => f (force x));
+fun force x = Exn.release (force_result x);
+
+fun force_list xs =
+  (List.app (fn x => if pending x then ignore (force_result x) else ()) xs;
+   map force xs);
+
+fun map f x = lazy_name "Lazy.map" (fn () => f (force x));
 
 
 (* future evaluation *)
diff -r 48cfbccaf3f4 -r cad55bc7e37d src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Thu Jun 22 21:48:57 2017 +0200
@@ -37,7 +37,7 @@
   val cancel_all: queue -> group list * Thread.thread list
   val finish: task -> queue -> bool * queue
   val enroll: Thread.thread -> string -> group -> queue -> task * queue
-  val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
+  val enqueue_passive: group -> string -> (unit -> bool) -> queue -> task * queue
   val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
   val extend: task -> (bool -> bool) -> queue -> queue option
   val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue
@@ -312,9 +312,9 @@
 
 (* enqueue *)
 
-fun enqueue_passive group abort (Queue {groups, jobs, urgent}) =
+fun enqueue_passive group name abort (Queue {groups, jobs, urgent}) =
   let
-    val task = new_task group "passive" NONE;
+    val task = new_task group name NONE;
     val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
     val jobs' = jobs |> Task_Graph.new_node (task, Passive abort);
   in (task, make_queue groups' jobs' urgent) end;
diff -r 48cfbccaf3f4 -r cad55bc7e37d src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/Isar/code.ML	Thu Jun 22 21:48:57 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 48cfbccaf3f4 -r cad55bc7e37d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Jun 22 21:48:57 2017 +0200
@@ -648,14 +648,10 @@
 val get_result = Result.get o Proof.context_of;
 val put_result = Proof.map_context o Result.put;
 
-fun timing_estimate include_head elem =
-  let val trs = Thy_Syntax.flat_element elem |> not include_head ? tl
+fun timing_estimate elem =
+  let val trs = tl (Thy_Syntax.flat_element elem)
   in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
 
-fun priority estimate =
-  if estimate = Time.zeroTime then ~1
-  else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
-
 fun proof_future_enabled estimate st =
   (case try proof_of st of
     NONE => false
@@ -670,8 +666,7 @@
     val st' =
       if Goal.future_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then
         (Execution.fork
-          {name = "Toplevel.diag", pos = pos_of tr,
-            pri = priority (timing_estimate true (Thy_Syntax.atom tr))}
+          {name = "Toplevel.diag", pos = pos_of tr, pri = ~1}
           (fn () => command tr st); st)
       else command tr st;
   in (Result (tr, st'), st') end;
@@ -683,7 +678,7 @@
       let
         val (head_result, st') = atom_result keywords head_tr st;
         val (body_elems, end_tr) = element_rest;
-        val estimate = timing_estimate false elem;
+        val estimate = timing_estimate elem;
       in
         if not (proof_future_enabled estimate st')
         then
@@ -698,7 +693,7 @@
             val future_proof =
               Proof.future_proof (fn state =>
                 Execution.fork
-                  {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = priority estimate}
+                  {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = ~1}
                   (fn () =>
                     let
                       val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
diff -r 48cfbccaf3f4 -r cad55bc7e37d src/Pure/PIDE/active.ML
--- a/src/Pure/PIDE/active.ML	Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/PIDE/active.ML	Thu Jun 22 21:48:57 2017 +0200
@@ -49,7 +49,7 @@
   let
     val i = serial ();
     fun abort () = Synchronized.change dialogs (Inttab.delete_safe i);
-    val promise = Future.promise abort : string future;
+    val promise = Future.promise_name "dialog" abort : string future;
     val _ = Synchronized.change dialogs (Inttab.update_new (i, promise));
     fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
   in (result_markup, promise) end;
diff -r 48cfbccaf3f4 -r cad55bc7e37d src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/PIDE/command.ML	Thu Jun 22 21:48:57 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 48cfbccaf3f4 -r cad55bc7e37d src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Jun 22 21:48:57 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 48cfbccaf3f4 -r cad55bc7e37d src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/Syntax/syntax.ML	Thu Jun 22 21:48:57 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 48cfbccaf3f4 -r cad55bc7e37d src/Pure/System/invoke_scala.ML
--- a/src/Pure/System/invoke_scala.ML	Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/System/invoke_scala.ML	Thu Jun 22 21:48:57 2017 +0200
@@ -31,7 +31,7 @@
   let
     val id = new_id ();
     fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
-    val promise = Future.promise abort : string future;
+    val promise = Future.promise_name "invoke_scala" abort : string future;
     val _ = Synchronized.change promises (Symtab.update (id, promise));
     val _ = Output.protocol_message (Markup.invoke_scala name id) [arg];
   in promise end;
diff -r 48cfbccaf3f4 -r cad55bc7e37d src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/more_thm.ML	Thu Jun 22 21:48:57 2017 +0200
@@ -645,7 +645,7 @@
   Proofs.map (fold (cons o Thm.trim_context) more_thms);
 
 fun consolidate_theory thy =
-  List.app (Thm.consolidate o Thm.transfer thy) (rev (Proofs.get thy));
+  Thm.consolidate (map (Thm.transfer thy) (rev (Proofs.get thy)));
 
 
 
diff -r 48cfbccaf3f4 -r cad55bc7e37d src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/proofterm.ML	Thu Jun 22 21:48:57 2017 +0200
@@ -43,7 +43,7 @@
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   val fold_body_thms: ({serial: serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
     proof_body list -> 'a -> 'a
-  val consolidate: proof_body -> unit
+  val consolidate: proof_body list -> unit
   val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
 
   val oracle_ord: oracle * oracle -> order
@@ -197,15 +197,16 @@
 fun join_thms (thms: pthm list) =
   Future.joins (map (thm_node_body o #2) thms);
 
-fun consolidate (PBody {thms, ...}) =
-  List.app (Lazy.force o thm_node_consolidate o #2) thms;
+val consolidate =
+  maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
+  #> Lazy.force_list #> ignore;
 
 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)};
+        in consolidate (join_thms thms) end)};
 
 
 (***** proof atoms *****)
@@ -1530,8 +1531,7 @@
 
 fun fulfill_norm_proof thy ps body0 =
   let
-    val _ = List.app (consolidate o #2) ps;
-    val _ = consolidate body0;
+    val _ = consolidate (map #2 ps @ [body0]);
     val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
     val oracles =
       unions_oracles
diff -r 48cfbccaf3f4 -r cad55bc7e37d src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Jun 22 16:49:01 2017 +0100
+++ b/src/Pure/thm.ML	Thu Jun 22 21:48:57 2017 +0200
@@ -86,7 +86,7 @@
   val proof_bodies_of: thm list -> proof_body list
   val proof_body_of: thm -> proof_body
   val proof_of: thm -> proof
-  val consolidate: thm -> unit
+  val consolidate: thm list -> unit
   val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool}
   val future: thm future -> cterm -> thm
   val derivation_closed: thm -> bool
@@ -598,7 +598,7 @@
 val proof_body_of = singleton proof_bodies_of;
 val proof_of = Proofterm.proof_of o proof_body_of;
 
-val consolidate = ignore o proof_bodies_of o single;
+val consolidate = ignore o proof_bodies_of;
 
 
 (* derivation status *)