# HG changeset patch
# User paulson
# Date 1527976664 -3600
# Node ID 0f19c98fa7be2a4b76fc5430621cc27cdccdb64b
# Parent  e761afd35baa3f9964aa58e94d6f3ec5f1940ab7# Parent  8cd3d0305269233d7a4588f4b0136f7df955f2c4
merged

diff -r 8cd3d0305269 -r 0f19c98fa7be NEWS
--- a/NEWS	Sat Jun 02 22:57:18 2018 +0100
+++ b/NEWS	Sat Jun 02 22:57:44 2018 +0100
@@ -380,6 +380,11 @@
 and concurrent use of theories, based on Isabelle/PIDE infrastructure.
 See also the "system" manual.
 
+* The command-line tool "dump" dumps information from the cumulative
+PIDE session database: many sessions may be loaded into a given logic
+image, results from all loaded theories are written to the output
+directory.
+
 * The command-line tool "isabelle update_comments" normalizes formal
 comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to
 approximate the appearance in document output). This is more specific
diff -r 8cd3d0305269 -r 0f19c98fa7be etc/options
--- a/etc/options	Sat Jun 02 22:57:18 2018 +0100
+++ b/etc/options	Sat Jun 02 22:57:44 2018 +0100
@@ -156,7 +156,7 @@
 public option editor_output_delay : real = 0.1
   -- "delay for prover output (markup, common messages etc.)"
 
-public option editor_consolidate_delay : real = 1.0
+public option editor_consolidate_delay : real = 2.5
   -- "delay to consolidate status of command evaluation (execution forks)"
 
 public option editor_prune_delay : real = 15
diff -r 8cd3d0305269 -r 0f19c98fa7be src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sat Jun 02 22:57:18 2018 +0100
+++ b/src/Doc/System/Sessions.thy	Sat Jun 02 22:57:44 2018 +0100
@@ -595,4 +595,85 @@
   own sub-directory hierarchy, using the session-qualified theory name.
 \<close>
 
+
+section \<open>Dump PIDE session database \label{sec:tool-dump}\<close>
+
+text \<open>
+  The @{tool_def "dump"} tool dumps information from the cumulative PIDE
+  session database (which is processed on the spot). Its command-line usage
+  is: @{verbatim [display]
+\<open>Usage: isabelle dump [OPTIONS] [SESSIONS ...]
+
+  Options are:
+    -A NAMES     dump named aspects (default: ...)
+    -B NAME      include session NAME and all descendants
+    -D DIR       include session directory and select its sessions
+    -O DIR       output directory for dumped files (default: "dump")
+    -R           operate on requirements of selected sessions
+    -X NAME      exclude sessions from group NAME and all descendants
+    -a           select all sessions
+    -d DIR       include session directory
+    -g NAME      select session group NAME
+    -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -s           system build mode for logic image
+    -v           verbose
+    -x NAME      exclude session NAME and all descendants
+
+  Dump cumulative PIDE session database, with the following aspects:
+    ...\<close>}
+
+  \<^medskip> Options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> and the
+  remaining command-line arguments specify sessions as in @{tool build}
+  (\secref{sec:tool-build}): the cumulative PIDE database of all their loaded
+  theories is dumped to the output directory of option \<^verbatim>\<open>-O\<close> (default: \<^verbatim>\<open>dump\<close>
+  in the current directory).
+
+  \<^medskip> Option \<^verbatim>\<open>-l\<close> specifies a logic image for the underlying prover process:
+  its theories are not processed again, and their PIDE session database is
+  excluded from the dump. Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close> when building
+  the logic image (\secref{sec:tool-build}).
+
+  \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
+  (\secref{sec:tool-build}).
+
+  \<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
+
+  \<^medskip> Option \<^verbatim>\<open>-A\<close> specifies named aspects of the dump, as a comma-separated
+  list. The default is to dump all known aspects, as given in the command-line
+  usage of the tool. The underlying Isabelle/Scala function
+  \<^verbatim>\<open>isabelle.Dump.dump()\<close> takes aspects as user-defined operations on the
+  final PIDE state and document version. This allows to imitate Prover IDE
+  rendering under program control.
+\<close>
+
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+  Dump all Isabelle/ZF sessions (which are rather small):
+  @{verbatim [display] \<open>isabelle dump -v -B ZF\<close>}
+
+  \<^smallskip>
+  Dump the quite substantial \<^verbatim>\<open>HOL-Analysis\<close> session, using main Isabelle/HOL
+  as starting point:
+  @{verbatim [display] \<open>isabelle dump -v -l HOL HOL-Analysis\<close>}
+
+  \<^smallskip>
+  Dump all sessions connected to HOL-Analysis, including a full bootstrap of
+  Isabelle/HOL from Isabelle/Pure:
+  @{verbatim [display] \<open>isabelle dump -v -l Pure -B HOL-Analysis\<close>}
+
+  This results in uniform PIDE markup for everything, except for the
+  Isabelle/Pure bootstrap process itself. Producing that on the spot requires
+  several GB of heap space, both for the Isabelle/Scala and Isabelle/ML
+  process (in 64bit mode). Here are some relevant settings (\secref{sec:boot})
+  for such ambitious applications:
+  @{verbatim [display]
+\<open>ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx32g -Xss16m"
+ML_OPTIONS="--minheap 4G --maxheap 32G"
+\<close>}
+
+\<close>
+
 end
diff -r 8cd3d0305269 -r 0f19c98fa7be src/HOL/Data_Structures/AVL_Set.thy
--- a/src/HOL/Data_Structures/AVL_Set.thy	Sat Jun 02 22:57:18 2018 +0100
+++ b/src/HOL/Data_Structures/AVL_Set.thy	Sat Jun 02 22:57:44 2018 +0100
@@ -455,7 +455,7 @@
 
 subsection \<open>Height-Size Relation\<close>
 
-text \<open>By Daniel St\"uwe, Manuel Eberl and Peter Lammich.\<close>
+text \<open>Based on theorems by Daniel St\"uwe, Manuel Eberl and Peter Lammich.\<close>
 
 lemma height_invers: 
   "(height t = 0) = (t = Leaf)"
@@ -529,19 +529,36 @@
 
 text \<open>The size of an AVL tree is (at least) exponential in its height:\<close>
 
-lemma avl_lowerbound:
+lemma avl_size_lowerbound:
   defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
   assumes "avl t"
-  shows   "real (size1 t) \<ge> \<phi> ^ (height t)"
+  shows   "\<phi> ^ (height t) \<le> size1 t"
 proof -
   have "\<phi> > 0" by(simp add: \<phi>_def add_pos_nonneg)
   hence "\<phi> ^ height t = (1 / \<phi> ^ 2) * \<phi> ^ (height t + 2)"
     by(simp add: field_simps power2_eq_square)
-  also have "\<dots> \<le> real (fib (height t + 2))"
+  also have "\<dots> \<le> fib (height t + 2)"
     using fib_lowerbound[of "height t + 2"] by(simp add: \<phi>_def)
-  also have "\<dots> \<le> real (size1 t)"
+  also have "\<dots> \<le> size1 t"
     using avl_fib_bound[of t "height t"] assms by simp
   finally show ?thesis .
 qed
 
+text \<open>The height of an AVL tree is most @{term "(1/log 2 \<phi>)"} \<open>\<approx> 1.44\<close> times worse
+than @{term "log 2 (size1 t)"}:\<close>
+
+lemma  avl_height_upperbound:
+  defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
+  assumes "avl t"
+  shows   "height t \<le> (1/log 2 \<phi>) * log 2 (size1 t)"
+proof -
+  have "\<phi> > 0" "\<phi> > 1" by(auto simp: \<phi>_def pos_add_strict)
+  hence "height t = log \<phi> (\<phi> ^ height t)" by(simp add: log_nat_power)
+  also have "\<dots> \<le> log \<phi> (size1 t)"
+    using avl_size_lowerbound[OF assms(2), folded \<phi>_def] \<open>1 < \<phi>\<close>  by simp
+  also have "\<dots> = (1/log 2 \<phi>) * log 2 (size1 t)"
+    by(simp add: log_base_change[of 2 \<phi>])
+  finally show ?thesis .
+qed
+
 end
diff -r 8cd3d0305269 -r 0f19c98fa7be src/HOL/HOLCF/Domain.thy
--- a/src/HOL/HOLCF/Domain.thy	Sat Jun 02 22:57:18 2018 +0100
+++ b/src/HOL/HOLCF/Domain.thy	Sat Jun 02 22:57:44 2018 +0100
@@ -341,12 +341,12 @@
 
 setup \<open>
   fold Domain_Take_Proofs.add_rec_type
-    [(@{type_name cfun}, [true, true]),
-     (@{type_name "sfun"}, [true, true]),
-     (@{type_name ssum}, [true, true]),
-     (@{type_name sprod}, [true, true]),
-     (@{type_name prod}, [true, true]),
-     (@{type_name "u"}, [true])]
+    [(\<^type_name>\<open>cfun\<close>, [true, true]),
+     (\<^type_name>\<open>sfun\<close>, [true, true]),
+     (\<^type_name>\<open>ssum\<close>, [true, true]),
+     (\<^type_name>\<open>sprod\<close>, [true, true]),
+     (\<^type_name>\<open>prod\<close>, [true, true]),
+     (\<^type_name>\<open>u\<close>, [true])]
 \<close>
 
 end
diff -r 8cd3d0305269 -r 0f19c98fa7be src/HOL/HOLCF/Map_Functions.thy
--- a/src/HOL/HOLCF/Map_Functions.thy	Sat Jun 02 22:57:18 2018 +0100
+++ b/src/HOL/HOLCF/Map_Functions.thy	Sat Jun 02 22:57:44 2018 +0100
@@ -188,14 +188,14 @@
 
 lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
   apply standard
-  subgoal for x by (cases x, simp, simp add: ep_pair.e_inverse)
-  subgoal for y by (cases y, simp, simp add: ep_pair.e_p_below)
+  subgoal for x by (cases x) (simp_all add: ep_pair.e_inverse)
+  subgoal for y by (cases y) (simp_all add: ep_pair.e_p_below)
   done
 
 lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)"
   apply standard
-  subgoal for x by (cases x, simp, simp add: deflation.idem)
-  subgoal for x by (cases x, simp, simp add: deflation.below)
+  subgoal for x by (cases x) (simp_all add: deflation.idem)
+  subgoal for x by (cases x) (simp_all add: deflation.below)
   done
 
 lemma finite_deflation_u_map:
@@ -235,12 +235,17 @@
   "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
     sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
      sprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
-  apply (induct p)
-   apply simp
-  apply (case_tac "f2\<cdot>x = \<bottom>", simp)
-  apply (case_tac "g2\<cdot>y = \<bottom>", simp)
-  apply simp
-  done
+proof (induct p)
+  case bottom
+  then show ?case by simp
+next
+  case (spair x y)
+  then show ?case
+    apply (cases "f2\<cdot>x = \<bottom>", simp)
+    apply (cases "g2\<cdot>y = \<bottom>", simp)
+    apply simp
+    done
+qed
 
 lemma ep_pair_sprod_map:
   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
@@ -251,11 +256,17 @@
   show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x
     by (induct x) simp_all
   show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y
-    apply (induct y)
-     apply simp
-    apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp)
-    apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below)
-    done
+  proof (induct y)
+    case bottom
+    then show ?case by simp
+  next
+    case (spair x y)
+    then show ?case
+      apply simp
+      apply (cases "p1\<cdot>x = \<bottom>", simp, cases "p2\<cdot>y = \<bottom>", simp)
+      apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below)
+      done
+  qed
 qed
 
 lemma deflation_sprod_map:
@@ -266,14 +277,24 @@
   interpret d2: deflation d2 by fact
   fix x
   show "sprod_map\<cdot>d1\<cdot>d2\<cdot>(sprod_map\<cdot>d1\<cdot>d2\<cdot>x) = sprod_map\<cdot>d1\<cdot>d2\<cdot>x"
-    apply (induct x, simp)
-    apply (case_tac "d1\<cdot>x = \<bottom>", simp, case_tac "d2\<cdot>y = \<bottom>", simp)
-    apply (simp add: d1.idem d2.idem)
-    done
+  proof (induct x)
+    case bottom
+    then show ?case by simp
+  next
+    case (spair x y)
+    then show ?case
+      apply (cases "d1\<cdot>x = \<bottom>", simp, cases "d2\<cdot>y = \<bottom>", simp)
+      apply (simp add: d1.idem d2.idem)
+      done
+  qed
   show "sprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
-    apply (induct x, simp)
-    apply (simp add: monofun_cfun d1.below d2.below)
-    done
+  proof (induct x)
+    case bottom
+    then show ?case by simp
+  next
+    case spair
+    then show ?case by (simp add: monofun_cfun d1.below d2.below)
+  qed
 qed
 
 lemma finite_deflation_sprod_map:
@@ -319,11 +340,16 @@
   "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow>
     ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) =
      ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
-  apply (induct p)
-    apply simp
-   apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp)
-  apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp)
-  done
+proof (induct p)
+  case bottom
+  then show ?case by simp
+next
+  case (sinl x)
+  then show ?case by (cases "f2\<cdot>x = \<bottom>") simp_all
+next
+  case (sinr y)
+  then show ?case by (cases "g2\<cdot>y = \<bottom>") simp_all
+qed
 
 lemma ep_pair_ssum_map:
   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
@@ -334,11 +360,16 @@
   show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x
     by (induct x) simp_all
   show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y
-    apply (induct y)
-      apply simp
-     apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below)
-    apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below)
-    done
+  proof (induct y)
+    case bottom
+    then show ?case by simp
+  next
+    case (sinl x)
+    then show ?case by (cases "p1\<cdot>x = \<bottom>") (simp_all add: e1p1.e_p_below)
+  next
+    case (sinr y)
+    then show ?case by (cases "p2\<cdot>y = \<bottom>") (simp_all add: e2p2.e_p_below)
+  qed
 qed
 
 lemma deflation_ssum_map:
@@ -349,15 +380,27 @@
   interpret d2: deflation d2 by fact
   fix x
   show "ssum_map\<cdot>d1\<cdot>d2\<cdot>(ssum_map\<cdot>d1\<cdot>d2\<cdot>x) = ssum_map\<cdot>d1\<cdot>d2\<cdot>x"
-    apply (induct x, simp)
-    apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.idem)
-    apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.idem)
-    done
+  proof (induct x)
+    case bottom
+    then show ?case by simp
+  next
+    case (sinl x)
+    then show ?case by (cases "d1\<cdot>x = \<bottom>") (simp_all add: d1.idem)
+  next
+    case (sinr y)
+    then show ?case by (cases "d2\<cdot>y = \<bottom>") (simp_all add: d2.idem)
+  qed
   show "ssum_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
-    apply (induct x, simp)
-    apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.below)
-    apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.below)
-    done
+  proof (induct x)
+    case bottom
+    then show ?case by simp
+  next
+    case (sinl x)
+    then show ?case by (cases "d1\<cdot>x = \<bottom>") (simp_all add: d1.below)
+  next
+    case (sinr y)
+    then show ?case by (cases "d2\<cdot>y = \<bottom>") (simp_all add: d2.below)
+  qed
 qed
 
 lemma finite_deflation_ssum_map:
diff -r 8cd3d0305269 -r 0f19c98fa7be src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Sat Jun 02 22:57:18 2018 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Sat Jun 02 22:57:44 2018 +0100
@@ -627,9 +627,10 @@
   "real_of_ereal y < x \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x)"
   by (cases y) auto
 
-(*To help with inferences like  a < ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y,
+text \<open>
+  To help with inferences like \<^prop>\<open>a < ereal x \<Longrightarrow> x < y \<Longrightarrow> a < ereal y\<close>,
   where x and y are real.
-*)
+\<close>
 
 lemma le_ereal_le: "a \<le> ereal x \<Longrightarrow> x \<le> y \<Longrightarrow> a \<le> ereal y"
   using ereal_less_eq(3) order.trans by blast
diff -r 8cd3d0305269 -r 0f19c98fa7be src/HOL/Library/Lub_Glb.thy
--- a/src/HOL/Library/Lub_Glb.thy	Sat Jun 02 22:57:18 2018 +0100
+++ b/src/HOL/Library/Lub_Glb.thy	Sat Jun 02 22:57:44 2018 +0100
@@ -221,7 +221,7 @@
 
 lemma isLub_mono_imp_LIMSEQ:
   fixes X :: "nat \<Rightarrow> real"
-  assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
+  assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use \<open>range X\<close> *)
   assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
   shows "X \<longlonglongrightarrow> u"
 proof -
diff -r 8cd3d0305269 -r 0f19c98fa7be src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Sat Jun 02 22:57:18 2018 +0100
+++ b/src/Pure/Concurrent/task_queue.ML	Sat Jun 02 22:57:44 2018 +0100
@@ -21,6 +21,7 @@
   val group_of_task: task -> group
   val name_of_task: task -> string
   val pri_of_task: task -> int
+  val eq_task: task * task -> bool
   val str_of_task: task -> string
   val str_of_task_groups: task -> string
   val task_statistics: task -> Properties.T
@@ -129,8 +130,11 @@
 
 fun group_of_task (Task {group, ...}) = group;
 fun name_of_task (Task {name, ...}) = name;
+fun id_of_task (Task {id, ...}) = id;
 fun pri_of_task (Task {pri, ...}) = the_default 0 pri;
 
+fun eq_task (task1, task2) = id_of_task task1 = id_of_task task2;
+
 fun str_of_task (Task {name, id, ...}) =
   if name = "" then string_of_int id else string_of_int id ^ " (" ^ name ^ ")";
 
diff -r 8cd3d0305269 -r 0f19c98fa7be src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat Jun 02 22:57:18 2018 +0100
+++ b/src/Pure/Isar/class.ML	Sat Jun 02 22:57:44 2018 +0100
@@ -375,12 +375,11 @@
   in (type_params, dangling_term_params) end;
 
 fun global_def (b, eq) thy =
-  thy
-  |> Thm.add_def_global false false (b, eq)
-  |>> (Thm.varifyT_global o snd)
-  |-> (fn def_thm => Global_Theory.store_thm (b, def_thm)
-      #> snd
-      #> pair def_thm);
+  let
+    val ((_, def_thm), thy') = thy |> Thm.add_def_global false false (b, eq);
+    val def_thm' = def_thm |> Thm.forall_intr_frees |> Thm.forall_elim_vars 0 |> Thm.varifyT_global;
+    val (_, thy'') = thy' |> Global_Theory.store_thm (b, def_thm');
+  in (def_thm', thy'') end;
 
 fun canonical_const class phi dangling_params ((b, mx), rhs) thy =
   let
diff -r 8cd3d0305269 -r 0f19c98fa7be src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sat Jun 02 22:57:18 2018 +0100
+++ b/src/Pure/PIDE/command.ML	Sat Jun 02 22:57:44 2018 +0100
@@ -22,10 +22,10 @@
   val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
     blob list * int -> Document_ID.command -> Token.T list -> eval -> eval
   type print
-  val print0: (unit -> unit) -> eval -> print
+  type print_fn = Toplevel.transition -> Toplevel.state -> unit
+  val print0: {pri: int, print_fn: print_fn} -> eval -> print
   val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
     eval -> print list -> print list option
-  type print_fn = Toplevel.transition -> Toplevel.state -> unit
   type print_function =
     {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} ->
       {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
@@ -342,9 +342,9 @@
 
 in
 
-fun print0 e =
+fun print0 {pri, print_fn} =
   make_print ("", [serial_string ()])
-    {delay = NONE, pri = 0, persistent = true, strict = true, print_fn = fn _ => fn _ => e ()};
+    {delay = NONE, pri = pri, persistent = true, strict = true, print_fn = print_fn};
 
 fun print command_visible command_overlays keywords command_name eval old_prints =
   let
diff -r 8cd3d0305269 -r 0f19c98fa7be src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Jun 02 22:57:18 2018 +0100
+++ b/src/Pure/PIDE/document.ML	Sat Jun 02 22:57:44 2018 +0100
@@ -497,7 +497,8 @@
             if Symtab.defined required name orelse visible_node node orelse pending_result node then
               let
                 fun body () =
-                  (if forall finished_import deps then
+                 (Execution.worker_task_active true;
+                  if forall finished_import deps then
                     iterate_entries (fn (_, opt_exec) => fn () =>
                       (case opt_exec of
                         SOME exec =>
@@ -505,13 +506,19 @@
                           then SOME (Command.exec execution_id exec)
                           else NONE
                       | NONE => NONE)) node ()
-                   else ())
-                   handle exn => (Output.system_message (Runtime.exn_message exn); Exn.reraise exn);
+                  else ();
+                  Execution.worker_task_active false)
+                  handle exn =>
+                   (Output.system_message (Runtime.exn_message exn);
+                    Execution.worker_task_active false;
+                    Exn.reraise exn);
                 val future =
                   (singleton o Future.forks)
                    {name = "theory:" ^ name,
                     group = SOME (Future.new_group NONE),
-                    deps = Future.task_of delay_request' :: maps (the_list o #2 o #2) deps,
+                    deps =
+                      Future.task_of delay_request' :: Execution.active_tasks name @
+                        maps (the_list o #2 o #2) deps,
                     pri = 0, interrupts = false} body;
               in (node, SOME (Future.task_of future)) end
             else (node, NONE));
@@ -707,17 +714,20 @@
                     adjust_pos = Position.adjust_offsets adjust,
                     segments = segments};
                 in
-                  fn () =>
+                  fn _ =>
                     (Thy_Info.apply_presentation presentation_context thy;
                      commit_consolidated node)
                 end
-              else fn () => commit_consolidated node;
+              else fn _ => commit_consolidated node;
 
             val result_entry =
               (case lookup_entry node result_id of
                 NONE => err_undef "result command entry" result_id
               | SOME (eval, prints) =>
-                  (result_id, SOME (eval, Command.print0 consolidation eval :: prints)));
+                  let
+                    val print = eval |> Command.print0
+                      {pri = Task_Queue.urgent_pri + 1, print_fn = K consolidation};
+                  in (result_id, SOME (eval, print :: prints)) end);
 
             val assign_update' = assign_update |> assign_update_change result_entry;
             val node' = node |> assign_entry result_entry;
diff -r 8cd3d0305269 -r 0f19c98fa7be src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Sat Jun 02 22:57:18 2018 +0100
+++ b/src/Pure/PIDE/execution.ML	Sat Jun 02 22:57:44 2018 +0100
@@ -10,6 +10,8 @@
   val start: unit -> Document_ID.execution
   val discontinue: unit -> unit
   val is_running: Document_ID.execution -> bool
+  val active_tasks: string -> Future.task list
+  val worker_task_active: bool -> string -> unit
   val is_running_exec: Document_ID.exec -> bool
   val running: Document_ID.execution -> Document_ID.exec -> Future.group list -> bool
   val snapshot: Document_ID.exec list -> Future.task list
@@ -31,17 +33,35 @@
 (* global state *)
 
 type print = {name: string, pri: int, body: unit -> unit};
-type exec_state = Future.group list * print list;  (*active forks, prints*)
-type state =
-  Document_ID.execution * (*overall document execution*)
-  exec_state Inttab.table;  (*running command execs*)
+type execs = (Future.group list * print list) (*active forks, prints*) Inttab.table;
+val init_execs: execs = Inttab.make [(Document_ID.none, ([], []))];
+
+datatype state =
+  State of
+   {execution_id: Document_ID.execution,  (*overall document execution*)
+    nodes: Future.task list Symtab.table,  (*active nodes*)
+    execs: execs};  (*running command execs*)
+
+fun make_state (execution_id, nodes, execs) =
+  State {execution_id = execution_id, nodes = nodes, execs = execs};
 
-val init_state: state = (Document_ID.none, Inttab.make [(Document_ID.none, ([], []))]);
-val state = Synchronized.var "Execution.state" init_state;
+local
+  val state =
+    Synchronized.var "Execution.state" (make_state (Document_ID.none, Symtab.empty, init_execs));
+in
+
+fun get_state () = let val State args = Synchronized.value state in args end;
 
-fun get_state () = Synchronized.value state;
-fun change_state_result f = Synchronized.change_result state f;
-fun change_state f = Synchronized.change state f;
+fun change_state_result f =
+  Synchronized.change_result state (fn (State {execution_id, nodes, execs}) =>
+    let val (result, args') = f (execution_id, nodes, execs)
+    in (result, make_state args') end);
+
+fun change_state f =
+  Synchronized.change state (fn (State {execution_id, nodes, execs}) =>
+    make_state (f (execution_id, nodes, execs)));
+
+end;
 
 fun unregistered exec_id = "Unregistered execution: " ^ Document_ID.print exec_id;
 
@@ -51,36 +71,52 @@
 fun start () =
   let
     val execution_id = Document_ID.make ();
-    val _ = change_state (apfst (K execution_id));
+    val _ = change_state (fn (_, nodes, execs) => (execution_id, nodes, execs));
   in execution_id end;
 
-fun discontinue () = change_state (apfst (K Document_ID.none));
+fun discontinue () =
+  change_state (fn (_, nodes, execs) => (Document_ID.none, nodes, execs));
+
+fun is_running execution_id =
+  execution_id = #execution_id (get_state ());
+
+
+(* active nodes *)
 
-fun is_running execution_id = execution_id = #1 (get_state ());
+fun active_tasks node_name =
+  Symtab.lookup_list (#nodes (get_state ())) node_name;
+
+fun worker_task_active insert node_name =
+  change_state (fn (execution_id, nodes, execs) =>
+    let
+      val nodes' = nodes
+        |> (if insert then Symtab.insert_list else Symtab.remove_list)
+          Task_Queue.eq_task (node_name, the (Future.worker_task ()));
+    in (execution_id, nodes', execs) end);
 
 
 (* running execs *)
 
 fun is_running_exec exec_id =
-  Inttab.defined (#2 (get_state ())) exec_id;
+  Inttab.defined (#execs (get_state ())) exec_id;
 
 fun running execution_id exec_id groups =
-  change_state_result (fn (execution_id', execs) =>
+  change_state_result (fn (execution_id', nodes, execs) =>
     let
       val ok = execution_id = execution_id' andalso not (Inttab.defined execs exec_id);
       val execs' = execs |> ok ? Inttab.update (exec_id, (groups, []));
-    in (ok, (execution_id', execs')) end);
+    in (ok, (execution_id', nodes, execs')) end);
 
 
 (* exec groups and tasks *)
 
-fun exec_groups ((_, execs): state) exec_id =
+fun exec_groups (execs: execs) exec_id =
   (case Inttab.lookup execs exec_id of
     SOME (groups, _) => groups
   | NONE => []);
 
 fun snapshot exec_ids =
-  change_state_result (`(fn state => Future.snapshot (maps (exec_groups state) exec_ids)));
+  change_state_result (`(fn (_, _, execs) => Future.snapshot (maps (exec_groups execs) exec_ids)));
 
 fun join exec_ids =
   (case snapshot exec_ids of
@@ -91,7 +127,7 @@
           deps = tasks, pri = 0, interrupts = false} I
       |> Future.join; join exec_ids));
 
-fun peek exec_id = exec_groups (get_state ()) exec_id;
+fun peek exec_id = exec_groups (#execs (get_state ())) exec_id;
 
 fun cancel exec_id = List.app Future.cancel_group (peek exec_id);
 
@@ -112,11 +148,12 @@
     let
       val exec_id = the_default 0 (Position.parse_id pos);
       val group = Future.worker_subgroup ();
-      val _ = change_state (apsnd (fn execs =>
+      val _ = change_state (fn (execution_id, nodes, execs) =>
         (case Inttab.lookup execs exec_id of
           SOME (groups, prints) =>
-            Inttab.update (exec_id, (group :: groups, prints)) execs
-        | NONE => raise Fail (unregistered exec_id))));
+            let val execs' = Inttab.update (exec_id, (group :: groups, prints)) execs
+            in (execution_id, nodes, execs') end
+        | NONE => raise Fail (unregistered exec_id)));
 
       val future =
         (singleton o Future.forks)
@@ -149,18 +186,20 @@
 (* print *)
 
 fun print ({name, pos, pri}: params) e =
-  change_state (apsnd (fn execs =>
+  change_state (fn (execution_id, nodes, execs) =>
     let
       val exec_id = the_default 0 (Position.parse_id pos);
       val print = {name = name, pri = pri, body = e};
     in
       (case Inttab.lookup execs exec_id of
-        SOME (groups, prints) => Inttab.update (exec_id, (groups, print :: prints)) execs
+        SOME (groups, prints) =>
+          let val execs' = Inttab.update (exec_id, (groups, print :: prints)) execs
+          in (execution_id, nodes, execs') end
       | NONE => raise Fail (unregistered exec_id))
-    end));
+    end);
 
 fun fork_prints exec_id =
-  (case Inttab.lookup (#2 (get_state ())) exec_id of
+  (case Inttab.lookup (#execs (get_state ())) exec_id of
     SOME (_, prints) =>
       if Future.relevant prints then
         let val pos = Position.thread_data () in
@@ -174,7 +213,7 @@
 (* cleanup *)
 
 fun purge exec_ids =
-  (change_state o apsnd) (fn execs =>
+  change_state (fn (execution_id, nodes, execs) =>
     let
       val execs' = fold Inttab.delete_safe exec_ids execs;
       val () =
@@ -183,12 +222,12 @@
           else groups |> List.app (fn group =>
             if Task_Queue.is_canceled group then ()
             else raise Fail ("Attempt to purge valid execution: " ^ Document_ID.print exec_id)));
-    in execs' end);
+    in (execution_id, nodes, execs') end);
 
 fun reset () =
-  change_state_result (fn (_, execs) =>
+  change_state_result (fn (_, _, execs) =>
     let val groups = Inttab.fold (append o #1 o #2) execs []
-    in (groups, init_state) end);
+    in (groups, (Document_ID.none, Symtab.empty, init_execs)) end);
 
 fun shutdown () =
   (Future.shutdown ();
@@ -197,4 +236,3 @@
     | exns => raise Par_Exn.make exns));
 
 end;
-
diff -r 8cd3d0305269 -r 0f19c98fa7be src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sat Jun 02 22:57:18 2018 +0100
+++ b/src/Pure/Thy/export_theory.scala	Sat Jun 02 22:57:44 2018 +0100
@@ -60,6 +60,8 @@
 
   /** theory content **/
 
+  val export_prefix: String = "theory/"
+
   sealed case class Theory(name: String, parents: List[String],
     types: List[Type],
     consts: List[Const],
@@ -100,7 +102,7 @@
     cache: Option[Term.Cache] = None): Theory =
   {
     val parents =
-      Export.read_entry(db, session_name, theory_name, "theory/parents") match {
+      Export.read_entry(db, session_name, theory_name, export_prefix + "parents") match {
         case Some(entry) => split_lines(entry.uncompressed().text)
         case None =>
           error("Missing theory export in session " + quote(session_name) + ": " +
@@ -147,7 +149,7 @@
   def read_export[A](db: SQL.Database, session_name: String, theory_name: String,
     export_name: String, decode: XML.Body => List[A]): List[A] =
   {
-    Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
+    Export.read_entry(db, session_name, theory_name, export_prefix + export_name) match {
       case Some(entry) => decode(entry.uncompressed_yxml())
       case None => Nil
     }
diff -r 8cd3d0305269 -r 0f19c98fa7be src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sat Jun 02 22:57:18 2018 +0100
+++ b/src/Pure/Tools/dump.scala	Sat Jun 02 22:57:44 2018 +0100
@@ -1,7 +1,7 @@
 /*  Title:      Pure/Tools/dump.scala
     Author:     Makarius
 
-Dump build database produced by PIDE session.
+Dump cumulative PIDE session database.
 */
 
 package isabelle
@@ -12,43 +12,68 @@
   /* aspects */
 
   sealed case class Aspect_Args(
-    options: Options, progress: Progress, output_dir: Path, result: Thy_Resources.Theories_Result)
+    options: Options,
+    progress: Progress,
+    output_dir: Path,
+    deps: Sessions.Deps,
+    result: Thy_Resources.Theories_Result)
   {
-    def write(node_name: Document.Node.Name, file_name: String, bytes: Bytes)
+    def write(node_name: Document.Node.Name, file_name: Path, bytes: Bytes)
     {
-      val path = output_dir + Path.basic(node_name.theory) + Path.basic(file_name)
+      val path = output_dir + Path.basic(node_name.theory) + file_name
       Isabelle_System.mkdirs(path.dir)
       Bytes.write(path, bytes)
     }
 
-    def write(node_name: Document.Node.Name, file_name: String, text: String): Unit =
+    def write(node_name: Document.Node.Name, file_name: Path, text: String): Unit =
       write(node_name, file_name, Bytes(text))
 
-    def write(node_name: Document.Node.Name, file_name: String, body: XML.Body): Unit =
+    def write(node_name: Document.Node.Name, file_name: Path, body: XML.Body): Unit =
       write(node_name, file_name, Symbol.encode(YXML.string_of_body(body)))
   }
 
-  sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit)
+  sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit,
+    options: List[String] = Nil)
+  {
+    override def toString: String = name
+  }
 
-  private val known_aspects =
+  val known_aspects =
     List(
       Aspect("messages", "output messages (YXML format)",
         { case args =>
             for (node_name <- args.result.node_names) {
-              args.write(node_name, "messages.yxml",
+              args.write(node_name, Path.explode("messages.yxml"),
                 args.result.messages(node_name).iterator.map(_._1).toList)
             }
         }),
       Aspect("markup", "PIDE markup (YXML format)",
         { case args =>
             for (node_name <- args.result.node_names) {
-              args.write(node_name, "markup.yxml", args.result.markup_to_XML(node_name))
+              args.write(node_name, Path.explode("markup.yxml"),
+                args.result.markup_to_XML(node_name))
             }
-        })
-    )
+        }),
+      Aspect("latex", "generated LaTeX source",
+        { case args =>
+            for {
+              node_name <- args.result.node_names
+              entry <- args.result.exports(node_name)
+              if entry.name == "document.tex"
+            } args.write(node_name, Path.explode(entry.name), entry.uncompressed())
+        }, options = List("editor_presentation")),
+      Aspect("theory", "foundational theory content",
+        { case args =>
+            for {
+              node_name <- args.result.node_names
+              entry <- args.result.exports(node_name)
+              if entry.name.startsWith(Export_Theory.export_prefix)
+            } args.write(node_name, Path.explode(entry.name), entry.uncompressed())
+        }, options = List("editor_presentation", "export_theory"))
+    ).sortBy(_.name)
 
   def show_aspects: String =
-    cat_lines(known_aspects.sortBy(_.name).map(aspect => aspect.name + " - " + aspect.description))
+    cat_lines(known_aspects.map(aspect => aspect.name + " - " + aspect.description))
 
   def the_aspect(name: String): Aspect =
     known_aspects.find(aspect => aspect.name == name) getOrElse
@@ -73,7 +98,9 @@
     if (Build.build_logic(options, logic, progress = progress, dirs = dirs,
       system_mode = system_mode) != 0) error(logic + " FAILED")
 
-    val dump_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", false)
+    val dump_options =
+      (options.int.update("completion_limit", 0).bool.update("ML_statistics", false) /: aspects)(
+        { case (opts, aspect) => (opts /: aspect.options)(_ + _) })
 
 
     /* dependencies */
@@ -102,7 +129,7 @@
 
     /* dump aspects */
 
-    val aspect_args = Aspect_Args(dump_options, progress, output_dir, theories_result)
+    val aspect_args = Aspect_Args(dump_options, progress, output_dir, deps, theories_result)
     aspects.foreach(_.operation(aspect_args))
 
     session_result
@@ -112,9 +139,9 @@
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
-    Isabelle_Tool("dump", "dump build database produced by PIDE session.", args =>
+    Isabelle_Tool("dump", "dump cumulative PIDE session database", args =>
     {
-      var aspects: List[Aspect] = Nil
+      var aspects: List[Aspect] = known_aspects
       var base_sessions: List[String] = Nil
       var select_dirs: List[Path] = Nil
       var output_dir = default_output_dir
@@ -133,7 +160,7 @@
 Usage: isabelle dump [OPTIONS] [SESSIONS ...]
 
   Options are:
-    -A NAMES     dump named aspects (comma-separated list, see below)
+    -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
     -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
@@ -148,8 +175,7 @@
     -v           verbose
     -x NAME      exclude session NAME and all descendants
 
-  Dump build database produced by PIDE session. The following dump aspects
-  are known (option -A):
+  Dump cumulative PIDE session database, with the following aspects:
 
 """ + Library.prefix_lines("    ", show_aspects) + "\n",
       "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),