diff --git a/src/HOL/Wfrec.thy b/src/HOL/Wfrec.thy
--- a/src/HOL/Wfrec.thy
+++ b/src/HOL/Wfrec.thy
@@ -1,112 +1,115 @@
 (*  Title:      HOL/Wfrec.thy
     Author:     Tobias Nipkow
     Author:     Lawrence C Paulson
     Author:     Konrad Slind
 *)
 
 section \<open>Well-Founded Recursion Combinator\<close>
 
 theory Wfrec
   imports Wellfounded
 begin
 
 inductive wfrec_rel :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" for R F
   where wfrecI: "(\<And>z. (z, x) \<in> R \<Longrightarrow> wfrec_rel R F z (g z)) \<Longrightarrow> wfrec_rel R F x (F g x)"
 
 definition cut :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
   where "cut f R x = (\<lambda>y. if (y, x) \<in> R then f y else undefined)"
 
 definition adm_wf :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> bool"
   where "adm_wf R F \<longleftrightarrow> (\<forall>f g x. (\<forall>z. (z, x) \<in> R \<longrightarrow> f z = g z) \<longrightarrow> F f x = F g x)"
 
 definition wfrec :: "('a \<times> 'a) set \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)) \<Rightarrow> ('a \<Rightarrow> 'b)"
   where "wfrec R F = (\<lambda>x. THE y. wfrec_rel R (\<lambda>f x. F (cut f R x) x) x y)"
 
 lemma cuts_eq: "(cut f R x = cut g R x) \<longleftrightarrow> (\<forall>y. (y, x) \<in> R \<longrightarrow> f y = g y)"
   by (simp add: fun_eq_iff cut_def)
 
 lemma cut_apply: "(x, a) \<in> R \<Longrightarrow> cut f R a x = f x"
   by (simp add: cut_def)
 
 text \<open>
   Inductive characterization of \<open>wfrec\<close> combinator; for details see:
   John Harrison, "Inductive definitions: automation and application".
 \<close>
 
 lemma theI_unique: "\<exists>!x. P x \<Longrightarrow> P x \<longleftrightarrow> x = The P"
   by (auto intro: the_equality[symmetric] theI)
 
 lemma wfrec_unique:
   assumes "adm_wf R F" "wf R"
   shows "\<exists>!y. wfrec_rel R F x y"
   using \<open>wf R\<close>
 proof induct
   define f where "f y = (THE z. wfrec_rel R F y z)" for y
   case (less x)
   then have "\<And>y z. (y, x) \<in> R \<Longrightarrow> wfrec_rel R F y z \<longleftrightarrow> z = f y"
     unfolding f_def by (rule theI_unique)
   with \<open>adm_wf R F\<close> show ?case
     by (subst wfrec_rel.simps) (auto simp: adm_wf_def)
 qed
 
 lemma adm_lemma: "adm_wf R (\<lambda>f x. F (cut f R x) x)"
   by (auto simp: adm_wf_def intro!: arg_cong[where f="\<lambda>x. F x y" for y] cuts_eq[THEN iffD2])
 
 lemma wfrec: "wf R \<Longrightarrow> wfrec R F a = F (cut (wfrec R F) R a) a"
   apply (simp add: wfrec_def)
   apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality])
    apply assumption
   apply (rule wfrec_rel.wfrecI)
   apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
   done
 
 
 text \<open>This form avoids giant explosions in proofs.  NOTE USE OF \<open>\<equiv>\<close>.\<close>
 lemma def_wfrec: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> f a = F (cut f R a) a"
   by (auto intro: wfrec)
 
 
 subsubsection \<open>Well-founded recursion via genuine fixpoints\<close>
 
 lemma wfrec_fixpoint:
   assumes wf: "wf R"
     and adm: "adm_wf R F"
   shows "wfrec R F = F (wfrec R F)"
 proof (rule ext)
   fix x
   have "wfrec R F x = F (cut (wfrec R F) R x) x"
     using wfrec[of R F] wf by simp
   also
   have "\<And>y. (y, x) \<in> R \<Longrightarrow> cut (wfrec R F) R x y = wfrec R F y"
     by (auto simp add: cut_apply)
   then have "F (cut (wfrec R F) R x) x = F (wfrec R F) x"
     using adm adm_wf_def[of R F] by auto
   finally show "wfrec R F x = F (wfrec R F) x" .
 qed
 
+lemma wfrec_def_adm: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> adm_wf R F \<Longrightarrow> f = F f"
+  using wfrec_fixpoint by simp
+
 
 subsection \<open>Wellfoundedness of \<open>same_fst\<close>\<close>
 
 definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set"
   where "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}"
    \<comment> \<open>For \<^const>\<open>wfrec\<close> declarations where the first n parameters
        stay unchanged in the recursive call.\<close>
 
 lemma same_fstI [intro!]: "P x \<Longrightarrow> (y', y) \<in> R x \<Longrightarrow> ((x, y'), (x, y)) \<in> same_fst P R"
   by (simp add: same_fst_def)
 
 lemma wf_same_fst:
   assumes "\<And>x. P x \<Longrightarrow> wf (R x)"
   shows "wf (same_fst P R)"
 proof (clarsimp simp add: wf_def same_fst_def)
   fix Q a b
   assume *: "\<forall>a b. (\<forall>x. P a \<and> (x,b) \<in> R a \<longrightarrow> Q (a,x)) \<longrightarrow> Q (a,b)"
   show "Q(a,b)"
   proof (cases "wf (R a)")
     case True
     then show ?thesis
       by (induction b rule: wf_induct_rule) (use * in blast)
   qed (use * assms in blast)
 qed
 
 end
diff --git a/src/HOL/Zorn.thy b/src/HOL/Zorn.thy
--- a/src/HOL/Zorn.thy
+++ b/src/HOL/Zorn.thy
@@ -1,910 +1,887 @@
 (*  Title:       HOL/Zorn.thy
     Author:      Jacques D. Fleuriot
     Author:      Tobias Nipkow, TUM
     Author:      Christian Sternagel, JAIST
 
 Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF).
-The well-ordering theorem.
 *)
 
-section \<open>Zorn's Lemma\<close>
+section \<open>Zorn's Lemma and the Well-ordering Theorem\<close>
 
 theory Zorn
   imports Order_Relation Hilbert_Choice
 begin
 
 subsection \<open>Zorn's Lemma for the Subset Relation\<close>
 
 subsubsection \<open>Results that do not require an order\<close>
 
 text \<open>Let \<open>P\<close> be a binary predicate on the set \<open>A\<close>.\<close>
 locale pred_on =
   fixes A :: "'a set"
     and P :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubset>" 50)
 begin
 
 abbreviation Peq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubseteq>" 50)
   where "x \<sqsubseteq> y \<equiv> P\<^sup>=\<^sup>= x y"
 
 text \<open>A chain is a totally ordered subset of \<open>A\<close>.\<close>
 definition chain :: "'a set \<Rightarrow> bool"
   where "chain C \<longleftrightarrow> C \<subseteq> A \<and> (\<forall>x\<in>C. \<forall>y\<in>C. x \<sqsubseteq> y \<or> y \<sqsubseteq> x)"
 
 text \<open>
   We call a chain that is a proper superset of some set \<open>X\<close>,
   but not necessarily a chain itself, a superchain of \<open>X\<close>.
 \<close>
 abbreviation superchain :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"  (infix "<c" 50)
   where "X <c C \<equiv> chain C \<and> X \<subset> C"
 
 text \<open>A maximal chain is a chain that does not have a superchain.\<close>
 definition maxchain :: "'a set \<Rightarrow> bool"
   where "maxchain C \<longleftrightarrow> chain C \<and> (\<nexists>S. C <c S)"
 
 text \<open>
   We define the successor of a set to be an arbitrary
   superchain, if such exists, or the set itself, otherwise.
 \<close>
 definition suc :: "'a set \<Rightarrow> 'a set"
   where "suc C = (if \<not> chain C \<or> maxchain C then C else (SOME D. C <c D))"
 
 lemma chainI [Pure.intro?]: "C \<subseteq> A \<Longrightarrow> (\<And>x y. x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x) \<Longrightarrow> chain C"
   unfolding chain_def by blast
 
 lemma chain_total: "chain C \<Longrightarrow> x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
   by (simp add: chain_def)
 
 lemma not_chain_suc [simp]: "\<not> chain X \<Longrightarrow> suc X = X"
   by (simp add: suc_def)
 
 lemma maxchain_suc [simp]: "maxchain X \<Longrightarrow> suc X = X"
   by (simp add: suc_def)
 
 lemma suc_subset: "X \<subseteq> suc X"
   by (auto simp: suc_def maxchain_def intro: someI2)
 
 lemma chain_empty [simp]: "chain {}"
   by (auto simp: chain_def)
 
 lemma not_maxchain_Some: "chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> C <c (SOME D. C <c D)"
   by (rule someI_ex) (auto simp: maxchain_def)
 
 lemma suc_not_equals: "chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> suc C \<noteq> C"
   using not_maxchain_Some by (auto simp: suc_def)
 
 lemma subset_suc:
   assumes "X \<subseteq> Y"
   shows "X \<subseteq> suc Y"
   using assms by (rule subset_trans) (rule suc_subset)
 
 text \<open>
   We build a set \<^term>\<open>\<C>\<close> that is closed under applications
   of \<^term>\<open>suc\<close> and contains the union of all its subsets.
 \<close>
 inductive_set suc_Union_closed ("\<C>")
   where
     suc: "X \<in> \<C> \<Longrightarrow> suc X \<in> \<C>"
   | Union [unfolded Pow_iff]: "X \<in> Pow \<C> \<Longrightarrow> \<Union>X \<in> \<C>"
 
 text \<open>
   Since the empty set as well as the set itself is a subset of
   every set, \<^term>\<open>\<C>\<close> contains at least \<^term>\<open>{} \<in> \<C>\<close> and
   \<^term>\<open>\<Union>\<C> \<in> \<C>\<close>.
 \<close>
 lemma suc_Union_closed_empty: "{} \<in> \<C>"
   and suc_Union_closed_Union: "\<Union>\<C> \<in> \<C>"
   using Union [of "{}"] and Union [of "\<C>"] by simp_all
 
 text \<open>Thus closure under \<^term>\<open>suc\<close> will hit a maximal chain
   eventually, as is shown below.\<close>
 
 lemma suc_Union_closed_induct [consumes 1, case_names suc Union, induct pred: suc_Union_closed]:
   assumes "X \<in> \<C>"
     and "\<And>X. X \<in> \<C> \<Longrightarrow> Q X \<Longrightarrow> Q (suc X)"
     and "\<And>X. X \<subseteq> \<C> \<Longrightarrow> \<forall>x\<in>X. Q x \<Longrightarrow> Q (\<Union>X)"
   shows "Q X"
   using assms by induct blast+
 
 lemma suc_Union_closed_cases [consumes 1, case_names suc Union, cases pred: suc_Union_closed]:
   assumes "X \<in> \<C>"
     and "\<And>Y. X = suc Y \<Longrightarrow> Y \<in> \<C> \<Longrightarrow> Q"
     and "\<And>Y. X = \<Union>Y \<Longrightarrow> Y \<subseteq> \<C> \<Longrightarrow> Q"
   shows "Q"
   using assms by cases simp_all
 
 text \<open>On chains, \<^term>\<open>suc\<close> yields a chain.\<close>
 lemma chain_suc:
   assumes "chain X"
   shows "chain (suc X)"
   using assms
   by (cases "\<not> chain X \<or> maxchain X") (force simp: suc_def dest: not_maxchain_Some)+
 
 lemma chain_sucD:
   assumes "chain X"
   shows "suc X \<subseteq> A \<and> chain (suc X)"
 proof -
   from \<open>chain X\<close> have *: "chain (suc X)"
     by (rule chain_suc)
   then have "suc X \<subseteq> A"
     unfolding chain_def by blast
   with * show ?thesis by blast
 qed
 
 lemma suc_Union_closed_total':
   assumes "X \<in> \<C>" and "Y \<in> \<C>"
     and *: "\<And>Z. Z \<in> \<C> \<Longrightarrow> Z \<subseteq> Y \<Longrightarrow> Z = Y \<or> suc Z \<subseteq> Y"
   shows "X \<subseteq> Y \<or> suc Y \<subseteq> X"
   using \<open>X \<in> \<C>\<close>
 proof induct
   case (suc X)
   with * show ?case by (blast del: subsetI intro: subset_suc)
 next
   case Union
   then show ?case by blast
 qed
 
 lemma suc_Union_closed_subsetD:
   assumes "Y \<subseteq> X" and "X \<in> \<C>" and "Y \<in> \<C>"
   shows "X = Y \<or> suc Y \<subseteq> X"
   using assms(2,3,1)
 proof (induct arbitrary: Y)
   case (suc X)
   note * = \<open>\<And>Y. Y \<in> \<C> \<Longrightarrow> Y \<subseteq> X \<Longrightarrow> X = Y \<or> suc Y \<subseteq> X\<close>
   with suc_Union_closed_total' [OF \<open>Y \<in> \<C>\<close> \<open>X \<in> \<C>\<close>]
   have "Y \<subseteq> X \<or> suc X \<subseteq> Y" by blast
   then show ?case
   proof
     assume "Y \<subseteq> X"
-    with * and \<open>Y \<in> \<C>\<close> have "X = Y \<or> suc Y \<subseteq> X" by blast
-    then show ?thesis
-    proof
-      assume "X = Y"
-      then show ?thesis by simp
-    next
-      assume "suc Y \<subseteq> X"
-      then have "suc Y \<subseteq> suc X" by (rule subset_suc)
-      then show ?thesis by simp
-    qed
+    with * and \<open>Y \<in> \<C>\<close> subset_suc show ?thesis
+      by fastforce
   next
     assume "suc X \<subseteq> Y"
     with \<open>Y \<subseteq> suc X\<close> show ?thesis by blast
   qed
 next
   case (Union X)
   show ?case
   proof (rule ccontr)
     assume "\<not> ?thesis"
     with \<open>Y \<subseteq> \<Union>X\<close> obtain x y z
       where "\<not> suc Y \<subseteq> \<Union>X"
         and "x \<in> X" and "y \<in> x" and "y \<notin> Y"
         and "z \<in> suc Y" and "\<forall>x\<in>X. z \<notin> x" by blast
     with \<open>X \<subseteq> \<C>\<close> have "x \<in> \<C>" by blast
     from Union and \<open>x \<in> X\<close> have *: "\<And>y. y \<in> \<C> \<Longrightarrow> y \<subseteq> x \<Longrightarrow> x = y \<or> suc y \<subseteq> x"
       by blast
     with suc_Union_closed_total' [OF \<open>Y \<in> \<C>\<close> \<open>x \<in> \<C>\<close>] have "Y \<subseteq> x \<or> suc x \<subseteq> Y"
       by blast
     then show False
     proof
       assume "Y \<subseteq> x"
-      with * [OF \<open>Y \<in> \<C>\<close>] have "x = Y \<or> suc Y \<subseteq> x" by blast
-      then show False
-      proof
-        assume "x = Y"
-        with \<open>y \<in> x\<close> and \<open>y \<notin> Y\<close> show False by blast
-      next
-        assume "suc Y \<subseteq> x"
-        with \<open>x \<in> X\<close> have "suc Y \<subseteq> \<Union>X" by blast
-        with \<open>\<not> suc Y \<subseteq> \<Union>X\<close> show False by contradiction
-      qed
+      with * [OF \<open>Y \<in> \<C>\<close>] \<open>y \<in> x\<close> \<open>y \<notin> Y\<close> \<open>x \<in> X\<close> \<open>\<not> suc Y \<subseteq> \<Union>X\<close> show False
+        by blast
     next
       assume "suc x \<subseteq> Y"
-      moreover from suc_subset and \<open>y \<in> x\<close> have "y \<in> suc x" by blast
-      ultimately show False using \<open>y \<notin> Y\<close> by blast
+      with \<open>y \<notin> Y\<close> suc_subset \<open>y \<in> x\<close> show False by blast
     qed
   qed
 qed
 
 text \<open>The elements of \<^term>\<open>\<C>\<close> are totally ordered by the subset relation.\<close>
 lemma suc_Union_closed_total:
   assumes "X \<in> \<C>" and "Y \<in> \<C>"
   shows "X \<subseteq> Y \<or> Y \<subseteq> X"
 proof (cases "\<forall>Z\<in>\<C>. Z \<subseteq> Y \<longrightarrow> Z = Y \<or> suc Z \<subseteq> Y")
   case True
   with suc_Union_closed_total' [OF assms]
   have "X \<subseteq> Y \<or> suc Y \<subseteq> X" by blast
   with suc_subset [of Y] show ?thesis by blast
 next
   case False
   then obtain Z where "Z \<in> \<C>" and "Z \<subseteq> Y" and "Z \<noteq> Y" and "\<not> suc Z \<subseteq> Y"
     by blast
   with suc_Union_closed_subsetD and \<open>Y \<in> \<C>\<close> show ?thesis
     by blast
 qed
 
 text \<open>Once we hit a fixed point w.r.t. \<^term>\<open>suc\<close>, all other elements
   of \<^term>\<open>\<C>\<close> are subsets of this fixed point.\<close>
 lemma suc_Union_closed_suc:
   assumes "X \<in> \<C>" and "Y \<in> \<C>" and "suc Y = Y"
   shows "X \<subseteq> Y"
   using \<open>X \<in> \<C>\<close>
 proof induct
   case (suc X)
   with \<open>Y \<in> \<C>\<close> and suc_Union_closed_subsetD have "X = Y \<or> suc X \<subseteq> Y"
     by blast
   then show ?case
     by (auto simp: \<open>suc Y = Y\<close>)
 next
   case Union
   then show ?case by blast
 qed
 
 lemma eq_suc_Union:
   assumes "X \<in> \<C>"
   shows "suc X = X \<longleftrightarrow> X = \<Union>\<C>"
     (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?lhs
   then have "\<Union>\<C> \<subseteq> X"
     by (rule suc_Union_closed_suc [OF suc_Union_closed_Union \<open>X \<in> \<C>\<close>])
   with \<open>X \<in> \<C>\<close> show ?rhs
     by blast
 next
   from \<open>X \<in> \<C>\<close> have "suc X \<in> \<C>" by (rule suc)
   then have "suc X \<subseteq> \<Union>\<C>" by blast
   moreover assume ?rhs
   ultimately have "suc X \<subseteq> X" by simp
   moreover have "X \<subseteq> suc X" by (rule suc_subset)
   ultimately show ?lhs ..
 qed
 
 lemma suc_in_carrier:
   assumes "X \<subseteq> A"
   shows "suc X \<subseteq> A"
   using assms
   by (cases "\<not> chain X \<or> maxchain X") (auto dest: chain_sucD)
 
 lemma suc_Union_closed_in_carrier:
   assumes "X \<in> \<C>"
   shows "X \<subseteq> A"
   using assms
   by induct (auto dest: suc_in_carrier)
 
 text \<open>All elements of \<^term>\<open>\<C>\<close> are chains.\<close>
 lemma suc_Union_closed_chain:
   assumes "X \<in> \<C>"
   shows "chain X"
   using assms
 proof induct
   case (suc X)
   then show ?case
     using not_maxchain_Some by (simp add: suc_def)
 next
   case (Union X)
   then have "\<Union>X \<subseteq> A"
     by (auto dest: suc_Union_closed_in_carrier)
   moreover have "\<forall>x\<in>\<Union>X. \<forall>y\<in>\<Union>X. x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
   proof (intro ballI)
     fix x y
     assume "x \<in> \<Union>X" and "y \<in> \<Union>X"
     then obtain u v where "x \<in> u" and "u \<in> X" and "y \<in> v" and "v \<in> X"
       by blast
     with Union have "u \<in> \<C>" and "v \<in> \<C>" and "chain u" and "chain v"
       by blast+
     with suc_Union_closed_total have "u \<subseteq> v \<or> v \<subseteq> u"
       by blast
     then show "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
     proof
       assume "u \<subseteq> v"
       from \<open>chain v\<close> show ?thesis
       proof (rule chain_total)
         show "y \<in> v" by fact
         show "x \<in> v" using \<open>u \<subseteq> v\<close> and \<open>x \<in> u\<close> by blast
       qed
     next
       assume "v \<subseteq> u"
       from \<open>chain u\<close> show ?thesis
       proof (rule chain_total)
         show "x \<in> u" by fact
         show "y \<in> u" using \<open>v \<subseteq> u\<close> and \<open>y \<in> v\<close> by blast
       qed
     qed
   qed
   ultimately show ?case unfolding chain_def ..
 qed
 
 subsubsection \<open>Hausdorff's Maximum Principle\<close>
 
 text \<open>There exists a maximal totally ordered subset of \<open>A\<close>. (Note that we do not
   require \<open>A\<close> to be partially ordered.)\<close>
 
 theorem Hausdorff: "\<exists>C. maxchain C"
 proof -
   let ?M = "\<Union>\<C>"
   have "maxchain ?M"
   proof (rule ccontr)
     assume "\<not> ?thesis"
     then have "suc ?M \<noteq> ?M"
       using suc_not_equals and suc_Union_closed_chain [OF suc_Union_closed_Union] by simp
     moreover have "suc ?M = ?M"
       using eq_suc_Union [OF suc_Union_closed_Union] by simp
     ultimately show False by contradiction
   qed
   then show ?thesis by blast
 qed
 
 text \<open>Make notation \<^term>\<open>\<C>\<close> available again.\<close>
 no_notation suc_Union_closed  ("\<C>")
 
 lemma chain_extend: "chain C \<Longrightarrow> z \<in> A \<Longrightarrow> \<forall>x\<in>C. x \<sqsubseteq> z \<Longrightarrow> chain ({z} \<union> C)"
   unfolding chain_def by blast
 
 lemma maxchain_imp_chain: "maxchain C \<Longrightarrow> chain C"
   by (simp add: maxchain_def)
 
 end
 
 text \<open>Hide constant \<^const>\<open>pred_on.suc_Union_closed\<close>, which was just needed
   for the proof of Hausforff's maximum principle.\<close>
 hide_const pred_on.suc_Union_closed
 
 lemma chain_mono:
   assumes "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> P x y \<Longrightarrow> Q x y"
     and "pred_on.chain A P C"
   shows "pred_on.chain A Q C"
   using assms unfolding pred_on.chain_def by blast
 
 
 subsubsection \<open>Results for the proper subset relation\<close>
 
 interpretation subset: pred_on "A" "(\<subset>)" for A .
 
 lemma subset_maxchain_max:
   assumes "subset.maxchain A C"
     and "X \<in> A"
     and "\<Union>C \<subseteq> X"
   shows "\<Union>C = X"
 proof (rule ccontr)
   let ?C = "{X} \<union> C"
   from \<open>subset.maxchain A C\<close> have "subset.chain A C"
     and *: "\<And>S. subset.chain A S \<Longrightarrow> \<not> C \<subset> S"
     by (auto simp: subset.maxchain_def)
   moreover have "\<forall>x\<in>C. x \<subseteq> X" using \<open>\<Union>C \<subseteq> X\<close> by auto
   ultimately have "subset.chain A ?C"
     using subset.chain_extend [of A C X] and \<open>X \<in> A\<close> by auto
   moreover assume **: "\<Union>C \<noteq> X"
   moreover from ** have "C \<subset> ?C" using \<open>\<Union>C \<subseteq> X\<close> by auto
   ultimately show False using * by blast
 qed
 
 lemma subset_chain_def: "\<And>\<A>. subset.chain \<A> \<C> = (\<C> \<subseteq> \<A> \<and> (\<forall>X\<in>\<C>. \<forall>Y\<in>\<C>. X \<subseteq> Y \<or> Y \<subseteq> X))"
   by (auto simp: subset.chain_def)
 
 lemma subset_chain_insert:
   "subset.chain \<A> (insert B \<B>) \<longleftrightarrow> B \<in> \<A> \<and> (\<forall>X\<in>\<B>. X \<subseteq> B \<or> B \<subseteq> X) \<and> subset.chain \<A> \<B>"
   by (fastforce simp add: subset_chain_def)
 
 subsubsection \<open>Zorn's lemma\<close>
 
 text \<open>If every chain has an upper bound, then there is a maximal set.\<close>
 theorem subset_Zorn:
   assumes "\<And>C. subset.chain A C \<Longrightarrow> \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U"
   shows "\<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
 proof -
   from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" ..
   then have "subset.chain A M"
     by (rule subset.maxchain_imp_chain)
   with assms obtain Y where "Y \<in> A" and "\<forall>X\<in>M. X \<subseteq> Y"
     by blast
   moreover have "\<forall>X\<in>A. Y \<subseteq> X \<longrightarrow> Y = X"
   proof (intro ballI impI)
     fix X
     assume "X \<in> A" and "Y \<subseteq> X"
     show "Y = X"
     proof (rule ccontr)
       assume "\<not> ?thesis"
       with \<open>Y \<subseteq> X\<close> have "\<not> X \<subseteq> Y" by blast
       from subset.chain_extend [OF \<open>subset.chain A M\<close> \<open>X \<in> A\<close>] and \<open>\<forall>X\<in>M. X \<subseteq> Y\<close>
       have "subset.chain A ({X} \<union> M)"
         using \<open>Y \<subseteq> X\<close> by auto
       moreover have "M \<subset> {X} \<union> M"
         using \<open>\<forall>X\<in>M. X \<subseteq> Y\<close> and \<open>\<not> X \<subseteq> Y\<close> by auto
       ultimately show False
         using \<open>subset.maxchain A M\<close> by (auto simp: subset.maxchain_def)
     qed
   qed
   ultimately show ?thesis by blast
 qed
 
 text \<open>Alternative version of Zorn's lemma for the subset relation.\<close>
 lemma subset_Zorn':
   assumes "\<And>C. subset.chain A C \<Longrightarrow> \<Union>C \<in> A"
   shows "\<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
 proof -
   from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" ..
   then have "subset.chain A M"
     by (rule subset.maxchain_imp_chain)
   with assms have "\<Union>M \<in> A" .
   moreover have "\<forall>Z\<in>A. \<Union>M \<subseteq> Z \<longrightarrow> \<Union>M = Z"
   proof (intro ballI impI)
     fix Z
     assume "Z \<in> A" and "\<Union>M \<subseteq> Z"
     with subset_maxchain_max [OF \<open>subset.maxchain A M\<close>]
       show "\<Union>M = Z" .
   qed
   ultimately show ?thesis by blast
 qed
 
 
 subsection \<open>Zorn's Lemma for Partial Orders\<close>
 
 text \<open>Relate old to new definitions.\<close>
 
 definition chain_subset :: "'a set set \<Rightarrow> bool"  ("chain\<^sub>\<subseteq>")  (* Define globally? In Set.thy? *)
   where "chain\<^sub>\<subseteq> C \<longleftrightarrow> (\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A)"
 
 definition chains :: "'a set set \<Rightarrow> 'a set set set"
   where "chains A = {C. C \<subseteq> A \<and> chain\<^sub>\<subseteq> C}"
 
 definition Chains :: "('a \<times> 'a) set \<Rightarrow> 'a set set"  (* Define globally? In Relation.thy? *)
   where "Chains r = {C. \<forall>a\<in>C. \<forall>b\<in>C. (a, b) \<in> r \<or> (b, a) \<in> r}"
 
 lemma chains_extend: "c \<in> chains S \<Longrightarrow> z \<in> S \<Longrightarrow> \<forall>x \<in> c. x \<subseteq> z \<Longrightarrow> {z} \<union> c \<in> chains S"
   for z :: "'a set"
   unfolding chains_def chain_subset_def by blast
 
 lemma mono_Chains: "r \<subseteq> s \<Longrightarrow> Chains r \<subseteq> Chains s"
   unfolding Chains_def by blast
 
 lemma chain_subset_alt_def: "chain\<^sub>\<subseteq> C = subset.chain UNIV C"
   unfolding chain_subset_def subset.chain_def by fast
 
 lemma chains_alt_def: "chains A = {C. subset.chain A C}"
   by (simp add: chains_def chain_subset_alt_def subset.chain_def)
 
 lemma Chains_subset: "Chains r \<subseteq> {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}"
   by (force simp add: Chains_def pred_on.chain_def)
 
 lemma Chains_subset':
   assumes "refl r"
   shows "{C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C} \<subseteq> Chains r"
   using assms
   by (auto simp add: Chains_def pred_on.chain_def refl_on_def)
 
 lemma Chains_alt_def:
   assumes "refl r"
   shows "Chains r = {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}"
   using assms Chains_subset Chains_subset' by blast
 
 lemma Chains_relation_of:
   assumes "C \<in> Chains (relation_of P A)" shows "C \<subseteq> A"
   using assms unfolding Chains_def relation_of_def by auto
 
 lemma pairwise_chain_Union:
   assumes P: "\<And>S. S \<in> \<C> \<Longrightarrow> pairwise R S" and "chain\<^sub>\<subseteq> \<C>"
   shows "pairwise R (\<Union>\<C>)"
   using \<open>chain\<^sub>\<subseteq> \<C>\<close> unfolding pairwise_def chain_subset_def
   by (blast intro: P [unfolded pairwise_def, rule_format])
 
 lemma Zorn_Lemma: "\<forall>C\<in>chains A. \<Union>C \<in> A \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
   using subset_Zorn' [of A] by (force simp: chains_alt_def)
 
 lemma Zorn_Lemma2: "\<forall>C\<in>chains A. \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
   using subset_Zorn [of A] by (auto simp: chains_alt_def)
 
 subsection \<open>Other variants of Zorn's Lemma\<close>
 
 lemma chainsD: "c \<in> chains S \<Longrightarrow> x \<in> c \<Longrightarrow> y \<in> c \<Longrightarrow> x \<subseteq> y \<or> y \<subseteq> x"
   unfolding chains_def chain_subset_def by blast
 
 lemma chainsD2: "c \<in> chains S \<Longrightarrow> c \<subseteq> S"
   unfolding chains_def by blast
 
 lemma Zorns_po_lemma:
   assumes po: "Partial_order r"
     and u: "\<And>C. C \<in> Chains r \<Longrightarrow> \<exists>u\<in>Field r. \<forall>a\<in>C. (a, u) \<in> r"
   shows "\<exists>m\<in>Field r. \<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m"
 proof -
   have "Preorder r"
     using po by (simp add: partial_order_on_def)
   txt \<open>Mirror \<open>r\<close> in the set of subsets below (wrt \<open>r\<close>) elements of \<open>A\<close>.\<close>
   let ?B = "\<lambda>x. r\<inverse> `` {x}"
   let ?S = "?B ` Field r"
   have "\<exists>u\<in>Field r. \<forall>A\<in>C. A \<subseteq> r\<inverse> `` {u}"  (is "\<exists>u\<in>Field r. ?P u")
     if 1: "C \<subseteq> ?S" and 2: "\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A" for C
   proof -
     let ?A = "{x\<in>Field r. \<exists>M\<in>C. M = ?B x}"
     from 1 have "C = ?B ` ?A" by (auto simp: image_def)
     have "?A \<in> Chains r"
     proof (simp add: Chains_def, intro allI impI, elim conjE)
       fix a b
       assume "a \<in> Field r" and "?B a \<in> C" and "b \<in> Field r" and "?B b \<in> C"
       with 2 have "?B a \<subseteq> ?B b \<or> ?B b \<subseteq> ?B a" by auto
       then show "(a, b) \<in> r \<or> (b, a) \<in> r"
         using \<open>Preorder r\<close> and \<open>a \<in> Field r\<close> and \<open>b \<in> Field r\<close>
         by (simp add:subset_Image1_Image1_iff)
     qed
     then obtain u where uA: "u \<in> Field r" "\<forall>a\<in>?A. (a, u) \<in> r"
       by (auto simp: dest: u)
     have "?P u"
     proof auto
       fix a B assume aB: "B \<in> C" "a \<in> B"
       with 1 obtain x where "x \<in> Field r" and "B = r\<inverse> `` {x}" by auto
       then show "(a, u) \<in> r"
         using uA and aB and \<open>Preorder r\<close>
         unfolding preorder_on_def refl_on_def by simp (fast dest: transD)
     qed
     then show ?thesis
       using \<open>u \<in> Field r\<close> by blast
   qed
   then have "\<forall>C\<in>chains ?S. \<exists>U\<in>?S. \<forall>A\<in>C. A \<subseteq> U"
     by (auto simp: chains_def chain_subset_def)
   from Zorn_Lemma2 [OF this] obtain m B
     where "m \<in> Field r"
       and "B = r\<inverse> `` {m}"
       and "\<forall>x\<in>Field r. B \<subseteq> r\<inverse> `` {x} \<longrightarrow> r\<inverse> `` {x} = B"
     by auto
   then have "\<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m"
     using po and \<open>Preorder r\<close> and \<open>m \<in> Field r\<close>
     by (auto simp: subset_Image1_Image1_iff Partial_order_eq_Image1_Image1_iff)
   then show ?thesis
     using \<open>m \<in> Field r\<close> by blast
 qed
 
 lemma predicate_Zorn:
   assumes po: "partial_order_on A (relation_of P A)"
     and ch: "\<And>C. C \<in> Chains (relation_of P A) \<Longrightarrow> \<exists>u \<in> A. \<forall>a \<in> C. P a u"
   shows "\<exists>m \<in> A. \<forall>a \<in> A. P m a \<longrightarrow> a = m"
 proof -
   have "a \<in> A" if "C \<in> Chains (relation_of P A)" and "a \<in> C" for C a
     using that unfolding Chains_def relation_of_def by auto
   moreover have "(a, u) \<in> relation_of P A" if "a \<in> A" and "u \<in> A" and "P a u" for a u
     unfolding relation_of_def using that by auto
   ultimately have "\<exists>m\<in>A. \<forall>a\<in>A. (m, a) \<in> relation_of P A \<longrightarrow> a = m"
     using Zorns_po_lemma[OF Partial_order_relation_ofI[OF po], rule_format] ch
     unfolding Field_relation_of[OF partial_order_onD(1)[OF po]] by blast
   then show ?thesis
     by (auto simp: relation_of_def)
 qed
 
 lemma Union_in_chain: "\<lbrakk>finite \<B>; \<B> \<noteq> {}; subset.chain \<A> \<B>\<rbrakk> \<Longrightarrow> \<Union>\<B> \<in> \<B>"
 proof (induction \<B> rule: finite_induct)
   case (insert B \<B>)
   show ?case
   proof (cases "\<B> = {}")
     case False
     then show ?thesis
       using insert sup.absorb2 by (auto simp: subset_chain_insert dest!: bspec [where x="\<Union>\<B>"])
   qed auto
 qed simp
 
 lemma Inter_in_chain: "\<lbrakk>finite \<B>; \<B> \<noteq> {}; subset.chain \<A> \<B>\<rbrakk> \<Longrightarrow> \<Inter>\<B> \<in> \<B>"
 proof (induction \<B> rule: finite_induct)
   case (insert B \<B>)
   show ?case
   proof (cases "\<B> = {}")
     case False
     then show ?thesis
       using insert inf.absorb2 by (auto simp: subset_chain_insert dest!: bspec [where x="\<Inter>\<B>"])
   qed auto
 qed simp
 
 lemma finite_subset_Union_chain:
   assumes "finite A" "A \<subseteq> \<Union>\<B>" "\<B> \<noteq> {}" and sub: "subset.chain \<A> \<B>"
   obtains B where "B \<in> \<B>" "A \<subseteq> B"
 proof -
   obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> \<B>" "A \<subseteq> \<Union>\<F>"
     using assms by (auto intro: finite_subset_Union)
   show thesis
   proof (cases "\<F> = {}")
     case True
     then show ?thesis
       using \<open>A \<subseteq> \<Union>\<F>\<close> \<open>\<B> \<noteq> {}\<close> that by fastforce
   next
     case False
     show ?thesis
     proof
       show "\<Union>\<F> \<in> \<B>"
         using sub \<open>\<F> \<subseteq> \<B>\<close> \<open>finite \<F>\<close>
         by (simp add: Union_in_chain False subset.chain_def subset_iff)
       show "A \<subseteq> \<Union>\<F>"
         using \<open>A \<subseteq> \<Union>\<F>\<close> by blast
     qed
   qed
 qed
 
 lemma subset_Zorn_nonempty:
   assumes "\<A> \<noteq> {}" and ch: "\<And>\<C>. \<lbrakk>\<C>\<noteq>{}; subset.chain \<A> \<C>\<rbrakk> \<Longrightarrow> \<Union>\<C> \<in> \<A>"
   shows "\<exists>M\<in>\<A>. \<forall>X\<in>\<A>. M \<subseteq> X \<longrightarrow> X = M"
 proof (rule subset_Zorn)
   show "\<exists>U\<in>\<A>. \<forall>X\<in>\<C>. X \<subseteq> U" if "subset.chain \<A> \<C>" for \<C>
   proof (cases "\<C> = {}")
     case True
     then show ?thesis
       using \<open>\<A> \<noteq> {}\<close> by blast
   next
     case False
     show ?thesis
       by (blast intro!: ch False that Union_upper)
   qed
 qed
 
 subsection \<open>The Well Ordering Theorem\<close>
 
 (* The initial segment of a relation appears generally useful.
    Move to Relation.thy?
    Definition correct/most general?
    Naming?
 *)
 definition init_seg_of :: "(('a \<times> 'a) set \<times> ('a \<times> 'a) set) set"
   where "init_seg_of = {(r, s). r \<subseteq> s \<and> (\<forall>a b c. (a, b) \<in> s \<and> (b, c) \<in> r \<longrightarrow> (a, b) \<in> r)}"
 
 abbreviation initial_segment_of_syntax :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"
     (infix "initial'_segment'_of" 55)
   where "r initial_segment_of s \<equiv> (r, s) \<in> init_seg_of"
 
 lemma refl_on_init_seg_of [simp]: "r initial_segment_of r"
   by (simp add: init_seg_of_def)
 
 lemma trans_init_seg_of:
   "r initial_segment_of s \<Longrightarrow> s initial_segment_of t \<Longrightarrow> r initial_segment_of t"
   by (simp (no_asm_use) add: init_seg_of_def) blast
 
 lemma antisym_init_seg_of: "r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r = s"
   unfolding init_seg_of_def by safe
 
 lemma Chains_init_seg_of_Union: "R \<in> Chains init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R"
   by (auto simp: init_seg_of_def Ball_def Chains_def) blast
 
 lemma chain_subset_trans_Union:
   assumes "chain\<^sub>\<subseteq> R" "\<forall>r\<in>R. trans r"
   shows "trans (\<Union>R)"
 proof (intro transI, elim UnionE)
   fix S1 S2 :: "'a rel" and x y z :: 'a
   assume "S1 \<in> R" "S2 \<in> R"
   with assms(1) have "S1 \<subseteq> S2 \<or> S2 \<subseteq> S1"
     unfolding chain_subset_def by blast
   moreover assume "(x, y) \<in> S1" "(y, z) \<in> S2"
   ultimately have "((x, y) \<in> S1 \<and> (y, z) \<in> S1) \<or> ((x, y) \<in> S2 \<and> (y, z) \<in> S2)"
     by blast
   with \<open>S1 \<in> R\<close> \<open>S2 \<in> R\<close> assms(2) show "(x, z) \<in> \<Union>R"
     by (auto elim: transE)
 qed
 
 lemma chain_subset_antisym_Union:
   assumes "chain\<^sub>\<subseteq> R" "\<forall>r\<in>R. antisym r"
   shows "antisym (\<Union>R)"
 proof (intro antisymI, elim UnionE)
   fix S1 S2 :: "'a rel" and x y :: 'a
   assume "S1 \<in> R" "S2 \<in> R"
   with assms(1) have "S1 \<subseteq> S2 \<or> S2 \<subseteq> S1"
     unfolding chain_subset_def by blast
   moreover assume "(x, y) \<in> S1" "(y, x) \<in> S2"
   ultimately have "((x, y) \<in> S1 \<and> (y, x) \<in> S1) \<or> ((x, y) \<in> S2 \<and> (y, x) \<in> S2)"
     by blast
   with \<open>S1 \<in> R\<close> \<open>S2 \<in> R\<close> assms(2) show "x = y"
     unfolding antisym_def by auto
 qed
 
 lemma chain_subset_Total_Union:
   assumes "chain\<^sub>\<subseteq> R" and "\<forall>r\<in>R. Total r"
   shows "Total (\<Union>R)"
 proof (simp add: total_on_def Ball_def, auto del: disjCI)
   fix r s a b
   assume A: "r \<in> R" "s \<in> R" "a \<in> Field r" "b \<in> Field s" "a \<noteq> b"
   from \<open>chain\<^sub>\<subseteq> R\<close> and \<open>r \<in> R\<close> and \<open>s \<in> R\<close> have "r \<subseteq> s \<or> s \<subseteq> r"
     by (auto simp add: chain_subset_def)
   then show "(\<exists>r\<in>R. (a, b) \<in> r) \<or> (\<exists>r\<in>R. (b, a) \<in> r)"
   proof
     assume "r \<subseteq> s"
     then have "(a, b) \<in> s \<or> (b, a) \<in> s"
       using assms(2) A mono_Field[of r s]
       by (auto simp add: total_on_def)
     then show ?thesis
       using \<open>s \<in> R\<close> by blast
   next
     assume "s \<subseteq> r"
     then have "(a, b) \<in> r \<or> (b, a) \<in> r"
       using assms(2) A mono_Field[of s r]
       by (fastforce simp add: total_on_def)
     then show ?thesis
       using \<open>r \<in> R\<close> by blast
   qed
 qed
 
 lemma wf_Union_wf_init_segs:
   assumes "R \<in> Chains init_seg_of"
     and "\<forall>r\<in>R. wf r"
   shows "wf (\<Union>R)"
 proof (simp add: wf_iff_no_infinite_down_chain, rule ccontr, auto)
   fix f
   assume 1: "\<forall>i. \<exists>r\<in>R. (f (Suc i), f i) \<in> r"
   then obtain r where "r \<in> R" and "(f (Suc 0), f 0) \<in> r" by auto
   have "(f (Suc i), f i) \<in> r" for i
   proof (induct i)
     case 0
     show ?case by fact
   next
     case (Suc i)
     then obtain s where s: "s \<in> R" "(f (Suc (Suc i)), f(Suc i)) \<in> s"
       using 1 by auto
     then have "s initial_segment_of r \<or> r initial_segment_of s"
       using assms(1) \<open>r \<in> R\<close> by (simp add: Chains_def)
     with Suc s show ?case by (simp add: init_seg_of_def) blast
   qed
   then show False
     using assms(2) and \<open>r \<in> R\<close>
     by (simp add: wf_iff_no_infinite_down_chain) blast
 qed
 
 lemma initial_segment_of_Diff: "p initial_segment_of q \<Longrightarrow> p - s initial_segment_of q - s"
   unfolding init_seg_of_def by blast
 
 lemma Chains_inits_DiffI: "R \<in> Chains init_seg_of \<Longrightarrow> {r - s |r. r \<in> R} \<in> Chains init_seg_of"
   unfolding Chains_def by (blast intro: initial_segment_of_Diff)
 
 theorem well_ordering: "\<exists>r::'a rel. Well_order r \<and> Field r = UNIV"
 proof -
 \<comment> \<open>The initial segment relation on well-orders:\<close>
   let ?WO = "{r::'a rel. Well_order r}"
   define I where "I = init_seg_of \<inter> ?WO \<times> ?WO"
   then have I_init: "I \<subseteq> init_seg_of" by simp
   then have subch: "\<And>R. R \<in> Chains I \<Longrightarrow> chain\<^sub>\<subseteq> R"
     unfolding init_seg_of_def chain_subset_def Chains_def by blast
   have Chains_wo: "\<And>R r. R \<in> Chains I \<Longrightarrow> r \<in> R \<Longrightarrow> Well_order r"
     by (simp add: Chains_def I_def) blast
   have FI: "Field I = ?WO"
     by (auto simp add: I_def init_seg_of_def Field_def)
   then have 0: "Partial_order I"
     by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def
         trans_def I_def elim!: trans_init_seg_of)
 \<comment> \<open>\<open>I\<close>-chains have upper bounds in \<open>?WO\<close> wrt \<open>I\<close>: their Union\<close>
   have "\<Union>R \<in> ?WO \<and> (\<forall>r\<in>R. (r, \<Union>R) \<in> I)" if "R \<in> Chains I" for R
   proof -
     from that have Ris: "R \<in> Chains init_seg_of"
       using mono_Chains [OF I_init] by blast
     have subch: "chain\<^sub>\<subseteq> R"
       using \<open>R \<in> Chains I\<close> I_init by (auto simp: init_seg_of_def chain_subset_def Chains_def)
     have "\<forall>r\<in>R. Refl r" and "\<forall>r\<in>R. trans r" and "\<forall>r\<in>R. antisym r"
       and "\<forall>r\<in>R. Total r" and "\<forall>r\<in>R. wf (r - Id)"
       using Chains_wo [OF \<open>R \<in> Chains I\<close>] by (simp_all add: order_on_defs)
     have "Refl (\<Union>R)"
       using \<open>\<forall>r\<in>R. Refl r\<close> unfolding refl_on_def by fastforce
     moreover have "trans (\<Union>R)"
       by (rule chain_subset_trans_Union [OF subch \<open>\<forall>r\<in>R. trans r\<close>])
     moreover have "antisym (\<Union>R)"
       by (rule chain_subset_antisym_Union [OF subch \<open>\<forall>r\<in>R. antisym r\<close>])
     moreover have "Total (\<Union>R)"
       by (rule chain_subset_Total_Union [OF subch \<open>\<forall>r\<in>R. Total r\<close>])
     moreover have "wf ((\<Union>R) - Id)"
     proof -
       have "(\<Union>R) - Id = \<Union>{r - Id | r. r \<in> R}" by blast
       with \<open>\<forall>r\<in>R. wf (r - Id)\<close> and wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]]
       show ?thesis by fastforce
     qed
     ultimately have "Well_order (\<Union>R)"
       by (simp add:order_on_defs)
     moreover have "\<forall>r \<in> R. r initial_segment_of \<Union>R"
       using Ris by (simp add: Chains_init_seg_of_Union)
     ultimately show ?thesis
       using mono_Chains [OF I_init] Chains_wo[of R] and \<open>R \<in> Chains I\<close>
       unfolding I_def by blast
   qed
   then have 1: "\<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" if "R \<in> Chains I" for R
     using that by (subst FI) blast
 \<comment> \<open>Zorn's Lemma yields a maximal well-order \<open>m\<close>:\<close>
   then obtain m :: "'a rel"
     where "Well_order m"
       and max: "\<forall>r. Well_order r \<and> (m, r) \<in> I \<longrightarrow> r = m"
     using Zorns_po_lemma[OF 0 1] unfolding FI by fastforce
 \<comment> \<open>Now show by contradiction that \<open>m\<close> covers the whole type:\<close>
   have False if "x \<notin> Field m" for x :: 'a
   proof -
 \<comment> \<open>Assuming that \<open>x\<close> is not covered and extend \<open>m\<close> at the top with \<open>x\<close>\<close>
     have "m \<noteq> {}"
     proof
       assume "m = {}"
       moreover have "Well_order {(x, x)}"
         by (simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def)
       ultimately show False using max
         by (auto simp: I_def init_seg_of_def simp del: Field_insert)
     qed
     then have "Field m \<noteq> {}" by (auto simp: Field_def)
     moreover have "wf (m - Id)"
       using \<open>Well_order m\<close> by (simp add: well_order_on_def)
 \<comment> \<open>The extension of \<open>m\<close> by \<open>x\<close>:\<close>
     let ?s = "{(a, x) | a. a \<in> Field m}"
     let ?m = "insert (x, x) m \<union> ?s"
     have Fm: "Field ?m = insert x (Field m)"
       by (auto simp: Field_def)
     have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)"
       using \<open>Well_order m\<close> by (simp_all add: order_on_defs)
 \<comment> \<open>We show that the extension is a well-order\<close>
     have "Refl ?m"
       using \<open>Refl m\<close> Fm unfolding refl_on_def by blast
     moreover have "trans ?m" using \<open>trans m\<close> and \<open>x \<notin> Field m\<close>
       unfolding trans_def Field_def by blast
     moreover have "antisym ?m"
       using \<open>antisym m\<close> and \<open>x \<notin> Field m\<close> unfolding antisym_def Field_def by blast
     moreover have "Total ?m"
       using \<open>Total m\<close> and Fm by (auto simp: total_on_def)
     moreover have "wf (?m - Id)"
     proof -
       have "wf ?s"
         using \<open>x \<notin> Field m\<close> by (auto simp: wf_eq_minimal Field_def Bex_def)
       then show ?thesis
         using \<open>wf (m - Id)\<close> and \<open>x \<notin> Field m\<close> wf_subset [OF \<open>wf ?s\<close> Diff_subset]
         by (auto simp: Un_Diff Field_def intro: wf_Un)
     qed
     ultimately have "Well_order ?m"
       by (simp add: order_on_defs)
 \<comment> \<open>We show that the extension is above \<open>m\<close>\<close>
     moreover have "(m, ?m) \<in> I"
       using \<open>Well_order ?m\<close> and \<open>Well_order m\<close> and \<open>x \<notin> Field m\<close>
       by (fastforce simp: I_def init_seg_of_def Field_def)
     ultimately
 \<comment> \<open>This contradicts maximality of \<open>m\<close>:\<close>
     show False
       using max and \<open>x \<notin> Field m\<close> unfolding Field_def by blast
   qed
   then have "Field m = UNIV" by auto
   with \<open>Well_order m\<close> show ?thesis by blast
 qed
 
 corollary well_order_on: "\<exists>r::'a rel. well_order_on A r"
 proof -
   obtain r :: "'a rel" where wo: "Well_order r" and univ: "Field r = UNIV"
     using well_ordering [where 'a = "'a"] by blast
   let ?r = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}"
   have 1: "Field ?r = A"
     using wo univ by (fastforce simp: Field_def order_on_defs refl_on_def)
   from \<open>Well_order r\<close> have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)"
     by (simp_all add: order_on_defs)
   from \<open>Refl r\<close> have "Refl ?r"
     by (auto simp: refl_on_def 1 univ)
   moreover from \<open>trans r\<close> have "trans ?r"
     unfolding trans_def by blast
   moreover from \<open>antisym r\<close> have "antisym ?r"
     unfolding antisym_def by blast
   moreover from \<open>Total r\<close> have "Total ?r"
     by (simp add:total_on_def 1 univ)
   moreover have "wf (?r - Id)"
     by (rule wf_subset [OF \<open>wf (r - Id)\<close>]) blast
   ultimately have "Well_order ?r"
     by (simp add: order_on_defs)
   with 1 show ?thesis by auto
 qed
 
-(* Move this to Hilbert Choice and wfrec to Wellfounded*)
-
-lemma wfrec_def_adm: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> adm_wf R F \<Longrightarrow> f = F f"
-  using wfrec_fixpoint by simp
-
 lemma dependent_wf_choice:
   fixes P :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   assumes "wf R"
     and adm: "\<And>f g x r. (\<And>z. (z, x) \<in> R \<Longrightarrow> f z = g z) \<Longrightarrow> P f x r = P g x r"
     and P: "\<And>x f. (\<And>y. (y, x) \<in> R \<Longrightarrow> P f y (f y)) \<Longrightarrow> \<exists>r. P f x r"
   shows "\<exists>f. \<forall>x. P f x (f x)"
 proof (intro exI allI)
   fix x
   define f where "f \<equiv> wfrec R (\<lambda>f x. SOME r. P f x r)"
   from \<open>wf R\<close> show "P f x (f x)"
   proof (induct x)
     case (less x)
     show "P f x (f x)"
     proof (subst (2) wfrec_def_adm[OF f_def \<open>wf R\<close>])
       show "adm_wf R (\<lambda>f x. SOME r. P f x r)"
-        by (auto simp add: adm_wf_def intro!: arg_cong[where f=Eps] ext adm)
+        by (auto simp: adm_wf_def intro!: arg_cong[where f=Eps] adm)
       show "P f x (Eps (P f x))"
         using P by (rule someI_ex) fact
     qed
   qed
 qed
 
 lemma (in wellorder) dependent_wellorder_choice:
   assumes "\<And>r f g x. (\<And>y. y < x \<Longrightarrow> f y = g y) \<Longrightarrow> P f x r = P g x r"
     and P: "\<And>x f. (\<And>y. y < x \<Longrightarrow> P f y (f y)) \<Longrightarrow> \<exists>r. P f x r"
   shows "\<exists>f. \<forall>x. P f x (f x)"
   using wf by (rule dependent_wf_choice) (auto intro!: assms)
 
 end
diff --git a/src/Pure/PIDE/document_status.scala b/src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala
+++ b/src/Pure/PIDE/document_status.scala
@@ -1,306 +1,306 @@
 /*  Title:      Pure/PIDE/document_status.scala
     Author:     Makarius
 
 Document status based on markup information.
 */
 
 package isabelle
 
 
 object Document_Status
 {
   /* command status */
 
   object Command_Status
   {
     val proper_elements: Markup.Elements =
       Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
         Markup.FINISHED, Markup.FAILED, Markup.CANCELED)
 
     val liberal_elements: Markup.Elements =
       proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
 
     def make(markup_iterator: Iterator[Markup]): Command_Status =
     {
       var touched = false
       var accepted = false
       var warned = false
       var failed = false
       var canceled = false
       var finalized = false
       var forks = 0
       var runs = 0
       for (markup <- markup_iterator) {
         markup.name match {
           case Markup.ACCEPTED => accepted = true
           case Markup.FORKED => touched = true; forks += 1
           case Markup.JOINED => forks -= 1
           case Markup.RUNNING => touched = true; runs += 1
           case Markup.FINISHED => runs -= 1
           case Markup.WARNING | Markup.LEGACY => warned = true
           case Markup.FAILED | Markup.ERROR => failed = true
           case Markup.CANCELED => canceled = true
           case Markup.FINALIZED => finalized = true
           case _ =>
         }
       }
       Command_Status(
         touched = touched,
         accepted = accepted,
         warned = warned,
         failed = failed,
         canceled = canceled,
         finalized = finalized,
         forks = forks,
         runs = runs)
     }
 
     val empty: Command_Status = make(Iterator.empty)
 
     def merge(status_iterator: Iterator[Command_Status]): Command_Status =
       if (status_iterator.hasNext) {
         val status0 = status_iterator.next()
         status_iterator.foldLeft(status0)(_ + _)
       }
       else empty
   }
 
   sealed case class Command_Status(
     private val touched: Boolean,
     private val accepted: Boolean,
     private val warned: Boolean,
     private val failed: Boolean,
     private val canceled: Boolean,
     private val finalized: Boolean,
     forks: Int,
     runs: Int)
   {
     def + (that: Command_Status): Command_Status =
       Command_Status(
         touched = touched || that.touched,
         accepted = accepted || that.accepted,
         warned = warned || that.warned,
         failed = failed || that.failed,
         canceled = canceled || that.canceled,
         finalized = finalized || that.finalized,
         forks = forks + that.forks,
         runs = runs + that.runs)
 
     def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
     def is_running: Boolean = runs != 0
     def is_warned: Boolean = warned
     def is_failed: Boolean = failed
     def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
     def is_canceled: Boolean = canceled
     def is_finalized: Boolean = finalized
     def is_terminated: Boolean = canceled || touched && forks == 0 && runs == 0
   }
 
 
   /* node status */
 
   object Node_Status
   {
     def make(
       state: Document.State,
       version: Document.Version,
       name: Document.Node.Name): Node_Status =
     {
       val node = version.nodes(name)
 
       var unprocessed = 0
       var running = 0
       var warned = 0
       var failed = 0
       var finished = 0
       var canceled = false
       var terminated = true
       var finalized = false
       for (command <- node.commands.iterator) {
         val states = state.command_states(version, command)
         val status = Command_Status.merge(states.iterator.map(_.document_status))
 
         if (status.is_running) running += 1
         else if (status.is_failed) failed += 1
         else if (status.is_warned) warned += 1
         else if (status.is_finished) finished += 1
         else unprocessed += 1
 
         if (status.is_canceled) canceled = true
         if (!status.is_terminated) terminated = false
         if (status.is_finalized) finalized = true
       }
       val initialized = state.node_initialized(version, name)
       val consolidated = state.node_consolidated(version, name)
 
       Node_Status(
         is_suppressed = version.nodes.is_suppressed(name),
         unprocessed = unprocessed,
         running = running,
         warned = warned,
         failed = failed,
         finished = finished,
         canceled = canceled,
         terminated = terminated,
         initialized = initialized,
         finalized = finalized,
         consolidated = consolidated)
     }
   }
 
   sealed case class Node_Status(
     is_suppressed: Boolean,
     unprocessed: Int,
     running: Int,
     warned: Int,
     failed: Int,
     finished: Int,
     canceled: Boolean,
     terminated: Boolean,
     initialized: Boolean,
     finalized: Boolean,
     consolidated: Boolean)
   {
     def ok: Boolean = failed == 0
     def total: Int = unprocessed + running + warned + failed + finished
 
     def quasi_consolidated: Boolean = !is_suppressed && !finalized && terminated
 
     def percentage: Int =
       if (consolidated) 100
       else if (total == 0) 0
       else (((total - unprocessed).toDouble / total) * 100).toInt min 99
 
     def json: JSON.Object.T =
       JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
         "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
         "canceled" -> canceled, "consolidated" -> consolidated,
         "percentage" -> percentage)
   }
 
 
   /* overall timing */
 
   object Overall_Timing
   {
     val empty: Overall_Timing = Overall_Timing(0.0, Map.empty)
 
     def make(
       state: Document.State,
       version: Document.Version,
       commands: Iterable[Command],
       threshold: Double = 0.0): Overall_Timing =
     {
       var total = 0.0
       var command_timings = Map.empty[Command, Double]
       for {
         command <- commands.iterator
         st <- state.command_states(version, command)
       } {
         val command_timing =
           st.status.foldLeft(0.0) {
             case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
             case (timing, _) => timing
           }
         total += command_timing
         if (command_timing > 0.0 && command_timing >= threshold) {
           command_timings += (command -> command_timing)
         }
       }
       Overall_Timing(total, command_timings)
     }
   }
 
   sealed case class Overall_Timing(total: Double, command_timings: Map[Command, Double])
   {
     def command_timing(command: Command): Double =
       command_timings.getOrElse(command, 0.0)
   }
 
 
   /* nodes status */
 
   object Overall_Node_Status extends Enumeration
   {
     val ok, failed, pending = Value
   }
 
   object Nodes_Status
   {
     val empty: Nodes_Status = new Nodes_Status(Map.empty, Document.Nodes.empty)
   }
 
   final class Nodes_Status private(
     private val rep: Map[Document.Node.Name, Node_Status],
     nodes: Document.Nodes)
   {
     def is_empty: Boolean = rep.isEmpty
     def apply(name: Document.Node.Name): Node_Status = rep(name)
     def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
 
     def present: List[(Document.Node.Name, Node_Status)] =
       (for {
         name <- nodes.topological_order.iterator
         node_status <- get(name)
       } yield (name, node_status)).toList
 
     def quasi_consolidated(name: Document.Node.Name): Boolean =
       rep.get(name) match {
         case Some(st) => st.quasi_consolidated
         case None => false
       }
 
     def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
       rep.get(name) match {
         case Some(st) if st.consolidated =>
           if (st.ok) Overall_Node_Status.ok else Overall_Node_Status.failed
         case _ => Overall_Node_Status.pending
       }
 
     def update(
       resources: Resources,
       state: Document.State,
       version: Document.Version,
       domain: Option[Set[Document.Node.Name]] = None,
       trim: Boolean = false): (Boolean, Nodes_Status) =
     {
       val nodes1 = version.nodes
       val update_iterator =
         for {
           name <- domain.getOrElse(nodes1.domain).iterator
-          if !resources.is_hidden(name) && !resources.session_base.loaded_theory(name)
+          if !Resources.hidden_node(name) && !resources.session_base.loaded_theory(name)
           st = Document_Status.Node_Status.make(state, version, name)
           if !rep.isDefinedAt(name) || rep(name) != st
         } yield (name -> st)
       val rep1 = rep ++ update_iterator
       val rep2 = if (trim) rep1 -- rep1.keysIterator.filterNot(nodes1.domain) else rep1
 
       (rep != rep2, new Nodes_Status(rep2, nodes1))
     }
 
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Nodes_Status => rep == other.rep
         case _ => false
       }
 
     override def toString: String =
     {
       var ok = 0
       var failed = 0
       var pending = 0
       var canceled = 0
       for (name <- rep.keysIterator) {
         overall_node_status(name) match {
           case Overall_Node_Status.ok => ok += 1
           case Overall_Node_Status.failed => failed += 1
           case Overall_Node_Status.pending => pending += 1
         }
         if (apply(name).canceled) canceled += 1
       }
       "Nodes_Status(ok = " + ok + ", failed = " + failed + ", pending = " + pending +
         ", canceled = " + canceled + ")"
     }
   }
 }
diff --git a/src/Pure/PIDE/resources.scala b/src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala
+++ b/src/Pure/PIDE/resources.scala
@@ -1,451 +1,454 @@
 /*  Title:      Pure/PIDE/resources.scala
     Author:     Makarius
 
 Resources for theories and auxiliary files.
 */
 
 package isabelle
 
 
 import scala.util.parsing.input.Reader
 
 import java.io.{File => JFile}
 
 
 object Resources
 {
   def empty: Resources =
     new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap)
+
+  def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name =
+    empty.file_node(file, dir = dir, theory = theory)
+
+  def hidden_node(name: Document.Node.Name): Boolean =
+    !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name)
+
+  def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] =
+    File_Format.registry.get(snapshot.node_name).flatMap(_.html_document(snapshot))
 }
 
 class Resources(
   val sessions_structure: Sessions.Structure,
   val session_base: Sessions.Base,
   val log: Logger = No_Logger,
   command_timings: List[Properties.T] = Nil)
 {
   resources =>
 
 
   /* init session */
 
   def init_session_yxml: String =
   {
     import XML.Encode._
 
     YXML.string_of_body(
       pair(list(pair(string, properties)),
       pair(list(pair(string, string)),
       pair(list(pair(string, list(string))),
       pair(list(properties),
       pair(list(pair(string, properties)),
       pair(list(pair(string, pair(bool, properties))),
       pair(list(pair(string, string)), list(string))))))))(
        (sessions_structure.session_positions,
        (sessions_structure.dest_session_directories,
        (sessions_structure.bibtex_entries,
        (command_timings,
        (Command_Span.load_commands.map(cmd => (cmd.name, cmd.position)),
        (Scala.functions.map(fun => (fun.name, (fun.multi, fun.position))),
        (session_base.global_theories.toList,
         session_base.loaded_theories.keys)))))))))
   }
 
 
   /* file formats */
 
   def make_theory_name(name: Document.Node.Name): Option[Document.Node.Name] =
     File_Format.registry.get(name).flatMap(_.make_theory_name(resources, name))
 
   def make_theory_content(thy_name: Document.Node.Name): Option[String] =
     File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name))
 
-  def is_hidden(name: Document.Node.Name): Boolean =
-    !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name)
-
-  def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] =
-    File_Format.registry.get(snapshot.node_name).flatMap(_.html_document(snapshot))
-
 
   /* file-system operations */
 
   def append(dir: String, source_path: Path): String =
     (Path.explode(dir) + source_path).expand.implode
 
   def append(node_name: Document.Node.Name, source_path: Path): String =
     append(node_name.master_dir, source_path)
 
   def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name =
   {
     val node = append(dir, file)
     val master_dir = append(dir, file.dir)
     Document.Node.Name(node, master_dir, theory)
   }
 
   def loaded_theory_node(theory: String): Document.Node.Name =
     Document.Node.Name(theory, "", theory)
 
 
   /* source files of Isabelle/ML bootstrap */
 
   def source_file(raw_name: String): Option[String] =
   {
     if (Path.is_wellformed(raw_name)) {
       if (Path.is_valid(raw_name)) {
         def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
 
         val path = Path.explode(raw_name)
         val path1 =
           if (path.is_absolute || path.is_current) check(path)
           else {
             check(Path.explode("~~/src/Pure") + path) orElse
               (if (Isabelle_System.getenv("ML_SOURCES") == "") None
                else check(Path.explode("$ML_SOURCES") + path))
           }
         Some(File.platform_path(path1 getOrElse path))
       }
       else None
     }
     else Some(raw_name)
   }
 
 
   /* theory files */
 
   def load_commands(syntax: Outer_Syntax, name: Document.Node.Name)
     : () => List[Command_Span.Span] =
   {
     val (is_utf8, raw_text) =
       with_thy_reader(name, reader => (Scan.reader_is_utf8(reader), reader.source.toString))
     () =>
       {
         if (syntax.has_load_commands(raw_text)) {
           val text = Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text))
           syntax.parse_spans(text).filter(_.is_load_command(syntax))
         }
         else Nil
       }
   }
 
   def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name, spans: List[Command_Span.Span])
     : List[Path] =
   {
     val dir = name.master_dir_path
     for { span <- spans; file <- span.loaded_files(syntax).files }
       yield (dir + Path.explode(file)).expand
   }
 
   def pure_files(syntax: Outer_Syntax): List[Path] =
   {
     val pure_dir = Path.explode("~~/src/Pure")
     for {
       (name, theory) <- Thy_Header.ml_roots
       path = (pure_dir + Path.explode(name)).expand
       node_name = Document.Node.Name(path.implode, path.dir.implode, theory)
       file <- loaded_files(syntax, node_name, load_commands(syntax, node_name)())
     } yield file
   }
 
   def theory_name(qualifier: String, theory: String): String =
     if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory))
       theory
     else Long_Name.qualify(qualifier, theory)
 
   def find_theory_node(theory: String): Option[Document.Node.Name] =
   {
     val thy_file = Path.basic(Long_Name.base_name(theory)).thy
     val session = session_base.theory_qualifier(theory)
     val dirs =
       sessions_structure.get(session) match {
         case Some(info) => info.dirs
         case None => Nil
       }
     dirs.collectFirst({
       case dir if (dir + thy_file).is_file => file_node(dir + thy_file, theory = theory) })
   }
 
   def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
   {
     val theory = theory_name(qualifier, Thy_Header.import_name(s))
     def theory_node = file_node(Path.explode(s).thy, dir = dir, theory = theory)
 
     if (!Thy_Header.is_base_name(s)) theory_node
     else if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
     else {
       find_theory_node(theory) match {
         case Some(node_name) => node_name
         case None => if (Long_Name.is_qualified(s)) loaded_theory_node(theory) else theory_node
       }
     }
   }
 
   def import_name(name: Document.Node.Name, s: String): Document.Node.Name =
     import_name(session_base.theory_qualifier(name), name.master_dir, s)
 
   def import_name(info: Sessions.Info, s: String): Document.Node.Name =
     import_name(info.name, info.dir.implode, s)
 
   def find_theory(file: JFile): Option[Document.Node.Name] =
   {
     for {
       qualifier <- session_base.session_directories.get(File.canonical(file).getParentFile)
       theory_base <- proper_string(Thy_Header.theory_name(file.getName))
       theory = theory_name(qualifier, theory_base)
       theory_node <- find_theory_node(theory)
       if File.eq(theory_node.path.file, file)
     } yield theory_node
   }
 
   def complete_import_name(context_name: Document.Node.Name, s: String): List[String] =
   {
     val context_session = session_base.theory_qualifier(context_name)
     val context_dir =
       try { Some(context_name.master_dir_path) }
       catch { case ERROR(_) => None }
     (for {
       (session, (info, _))  <- sessions_structure.imports_graph.iterator
       dir <- (if (session == context_session) context_dir.toList else info.dirs).iterator
       theory <- Thy_Header.try_read_dir(dir).iterator
       if Completion.completed(s)(theory)
     } yield {
       if (session == context_session || session_base.global_theories.isDefinedAt(theory)) theory
       else Long_Name.qualify(session, theory)
     }).toList.sorted
   }
 
   def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
     val path = name.path
     if (path.is_file) using(Scan.byte_reader(path.file))(f)
     else if (name.node == name.theory)
       error("Cannot load theory " + quote(name.theory))
     else error ("Cannot load theory file " + path)
   }
 
   def check_thy(node_name: Document.Node.Name, reader: Reader[Char],
     command: Boolean = true, strict: Boolean = true): Document.Node.Header =
   {
     if (node_name.is_theory && reader.source.length > 0) {
       try {
         val header = Thy_Header.read(node_name, reader, command = command, strict = strict)
         val imports =
           header.imports.map({ case (s, pos) =>
             val name = import_name(node_name, s)
             if (Sessions.exclude_theory(name.theory_base_name))
               error("Bad theory name " + quote(name.theory_base_name) + Position.here(pos))
             (name, pos)
           })
         Document.Node.Header(imports, header.keywords, header.abbrevs)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
     }
     else Document.Node.no_header
   }
 
 
   /* special header */
 
   def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
   {
     val imports =
       if (name.theory == Sessions.root_name) List(import_name(name, Sessions.theory_name))
       else if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP))
       else if (Thy_Header.is_bootstrap(name.theory)) List(import_name(name, Thy_Header.PURE))
       else Nil
     if (imports.isEmpty) None
     else Some(Document.Node.Header(imports.map((_, Position.none))))
   }
 
 
   /* blobs */
 
   def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
     (for {
       (node_name, node) <- nodes.iterator
       if !session_base.loaded_theory(node_name)
       cmd <- node.load_commands.iterator
       name <- cmd.blobs_undefined.iterator
     } yield name).toList
 
 
   /* document changes */
 
   def parse_change(
       reparse_limit: Int,
       previous: Document.Version,
       doc_blobs: Document.Blobs,
       edits: List[Document.Edit_Text],
       consolidate: List[Document.Node.Name]): Session.Change =
     Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate)
 
   def commit(change: Session.Change): Unit = {}
 
 
   /* theory and file dependencies */
 
   def dependencies(
       thys: List[(Document.Node.Name, Position.T)],
       progress: Progress = new Progress): Dependencies[Unit] =
     Dependencies.empty[Unit].require_thys((), thys, progress = progress)
 
   def session_dependencies(info: Sessions.Info, progress: Progress = new Progress)
     : Dependencies[Options] =
   {
     info.theories.foldLeft(Dependencies.empty[Options]) {
       case (dependencies, (options, thys)) =>
         dependencies.require_thys(options,
           for { (thy, pos) <- thys } yield (import_name(info, thy), pos),
           progress = progress)
     }
   }
 
   object Dependencies
   {
     def empty[A]: Dependencies[A] = new Dependencies[A](Nil, Map.empty)
 
     private def show_path(names: List[Document.Node.Name]): String =
       names.map(name => quote(name.theory)).mkString(" via ")
 
     private def cycle_msg(names: List[Document.Node.Name]): String =
       "Cyclic dependency of " + show_path(names)
 
     private def required_by(initiators: List[Document.Node.Name]): String =
       if (initiators.isEmpty) ""
       else "\n(required by " + show_path(initiators.reverse) + ")"
   }
 
   final class Dependencies[A] private(
     rev_entries: List[Document.Node.Entry],
     seen: Map[Document.Node.Name, A])
   {
     private def cons(entry: Document.Node.Entry): Dependencies[A] =
       new Dependencies[A](entry :: rev_entries, seen)
 
     def require_thy(adjunct: A,
       thy: (Document.Node.Name, Position.T),
       initiators: List[Document.Node.Name] = Nil,
       progress: Progress = new Progress): Dependencies[A] =
     {
       val (name, pos) = thy
 
       def message: String =
         "The error(s) above occurred for theory " + quote(name.theory) +
           Dependencies.required_by(initiators) + Position.here(pos)
 
       if (seen.isDefinedAt(name)) this
       else {
         val dependencies1 = new Dependencies[A](rev_entries, seen + (name -> adjunct))
         if (session_base.loaded_theory(name)) dependencies1
         else {
           try {
             if (initiators.contains(name)) error(Dependencies.cycle_msg(initiators))
 
             progress.expose_interrupt()
             val header =
               try {
                 with_thy_reader(name, check_thy(name, _, command = false)).cat_errors(message)
               }
               catch { case ERROR(msg) => cat_error(msg, message) }
             val entry = Document.Node.Entry(name, header)
             dependencies1.require_thys(adjunct, header.imports_pos,
               initiators = name :: initiators, progress = progress).cons(entry)
           }
           catch {
             case e: Throwable =>
               dependencies1.cons(Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))))
           }
         }
       }
     }
 
     def require_thys(adjunct: A,
         thys: List[(Document.Node.Name, Position.T)],
         progress: Progress = new Progress,
         initiators: List[Document.Node.Name] = Nil): Dependencies[A] =
       thys.foldLeft(this)(_.require_thy(adjunct, _, progress = progress, initiators = initiators))
 
     def entries: List[Document.Node.Entry] = rev_entries.reverse
 
     def theories: List[Document.Node.Name] = entries.map(_.name)
     def theories_adjunct: List[(Document.Node.Name, A)] = theories.map(name => (name, seen(name)))
 
     def errors: List[String] = entries.flatMap(_.header.errors)
 
     def check_errors: Dependencies[A] =
       errors match {
         case Nil => this
         case errs => error(cat_lines(errs))
       }
 
     lazy val theory_graph: Document.Node.Name.Graph[Unit] =
     {
       val regular = theories.toSet
       val irregular =
         (for {
           entry <- entries.iterator
           imp <- entry.header.imports
           if !regular(imp)
         } yield imp).toSet
 
       Document.Node.Name.make_graph(
         irregular.toList.map(name => ((name, ()), Nil)) :::
         entries.map(entry => ((entry.name, ()), entry.header.imports)))
     }
 
     lazy val loaded_theories: Graph[String, Outer_Syntax] =
       entries.foldLeft(session_base.loaded_theories) {
         case (graph, entry) =>
           val name = entry.name.theory
           val imports = entry.header.imports.map(_.theory)
 
           val graph1 = (name :: imports).foldLeft(graph)(_.default_node(_, Outer_Syntax.empty))
           val graph2 = imports.foldLeft(graph1)(_.add_edge(_, name))
 
           val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil
           val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node)
           val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header
 
           graph2.map_node(name, _ => syntax)
       }
 
     def get_syntax(name: Document.Node.Name): Outer_Syntax =
       loaded_theories.get_node(name.theory)
 
     def load_commands: List[(Document.Node.Name, List[Command_Span.Span])] =
       theories.zip(
         Par_List.map((e: () => List[Command_Span.Span]) => e(),
           theories.map(name => resources.load_commands(get_syntax(name), name))))
       .filter(p => p._2.nonEmpty)
 
     def loaded_files(name: Document.Node.Name, spans: List[Command_Span.Span])
       : (String, List[Path]) =
     {
       val theory = name.theory
       val syntax = get_syntax(name)
       val files1 = resources.loaded_files(syntax, name, spans)
       val files2 = if (theory == Thy_Header.PURE) pure_files(syntax) else Nil
       (theory, files1 ::: files2)
     }
 
     def loaded_files: List[Path] =
       for {
         (name, spans) <- load_commands
         file <- loaded_files(name, spans)._2
       } yield file
 
     def imported_files: List[Path] =
     {
       val base_theories =
         loaded_theories.all_preds(theories.map(_.theory)).
           filter(session_base.loaded_theories.defined)
 
       base_theories.map(theory => session_base.known_theories(theory).name.path) :::
       base_theories.flatMap(session_base.known_loaded_files.withDefaultValue(Nil))
     }
 
     lazy val overall_syntax: Outer_Syntax =
       Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node))
 
     override def toString: String = entries.toString
   }
 }
diff --git a/src/Pure/Thy/html.scala b/src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala
+++ b/src/Pure/Thy/html.scala
@@ -1,440 +1,441 @@
 /*  Title:      Pure/Thy/html.scala
     Author:     Makarius
 
 HTML presentation elements.
 */
 
 package isabelle
 
 
 object HTML
 {
   /* attributes */
 
   class Attribute(val name: String, value: String)
   {
     def xml: XML.Attribute = name -> value
     def apply(elem: XML.Elem): XML.Elem = elem + xml
   }
 
   def id(s: String): Attribute = new Attribute("id", s)
   def class_(name: String): Attribute = new Attribute("class", name)
 
   def width(w: Int): Attribute = new Attribute("width", w.toString)
   def height(h: Int): Attribute = new Attribute("height", h.toString)
   def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem))
 
   val entity_def: Attribute = class_("entity_def")
   val entity_ref: Attribute = class_("entity_ref")
 
 
   /* structured markup operators */
 
   def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
   val break: XML.Body = List(XML.elem("br"))
   val nl: XML.Body = List(XML.Text("\n"))
 
   class Operator(val name: String)
   {
     def apply(body: XML.Body): XML.Elem = XML.elem(name, body)
     def apply(att: Attribute, body: XML.Body): XML.Elem = att(apply(body))
     def apply(c: String, body: XML.Body): XML.Elem = apply(class_(c), body)
   }
 
   class Heading(name: String) extends Operator(name)
   {
     def apply(txt: String): XML.Elem = super.apply(text(txt))
     def apply(att: Attribute, txt: String): XML.Elem = super.apply(att, text(txt))
     def apply(c: String, txt: String): XML.Elem = super.apply(c, text(txt))
   }
 
   val div = new Operator("div")
   val span = new Operator("span")
   val pre = new Operator("pre")
   val par = new Operator("p")
   val sub = new Operator("sub")
   val sup = new Operator("sup")
   val emph = new Operator("em")
   val bold = new Operator("b")
   val code = new Operator("code")
   val item = new Operator("li")
   val list = new Operator("ul")
   val `enum` = new Operator("ol")
   val descr = new Operator("dl")
   val dt = new Operator("dt")
   val dd = new Operator("dd")
 
   val title = new Heading("title")
   val chapter = new Heading("h1")
   val section = new Heading("h2")
   val subsection = new Heading("h3")
   val subsubsection = new Heading("h4")
   val paragraph = new Heading("h5")
   val subparagraph = new Heading("h6")
 
   def itemize(items: List[XML.Body]): XML.Elem = list(items.map(item(_)))
   def enumerate(items: List[XML.Body]): XML.Elem = `enum`(items.map(item(_)))
   def description(items: List[(XML.Body, XML.Body)]): XML.Elem =
     descr(items.flatMap({ case (x, y) => List(dt(x), dd(y)) }))
 
   def link(href: String, body: XML.Body): XML.Elem =
     XML.Elem(Markup("a", List("href" -> href)), if (body.isEmpty) text(href) else body)
 
   def link(path: Path, body: XML.Body): XML.Elem = link(path.implode, body)
 
   def image(src: String, alt: String = ""): XML.Elem =
     XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
 
   def source(body: XML.Body): XML.Elem = pre("source", body)
   def source(src: String): XML.Elem = source(text(src))
 
   def style(s: String): XML.Elem = XML.elem("style", text(s))
   def style_file(href: String): XML.Elem =
     XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)
   def style_file(path: Path): XML.Elem = style_file(Url.print_file(path.file))
 
   def script(s: String): XML.Elem = XML.elem("script", text(s))
   def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil)
   def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file))
 
 
   /* output text with control symbols */
 
   private val control: Map[Symbol.Symbol, Operator] =
     Map(
       Symbol.sub -> sub, Symbol.sub_decoded -> sub,
       Symbol.sup -> sup, Symbol.sup_decoded -> sup,
       Symbol.bold -> bold, Symbol.bold_decoded -> bold)
 
   private val control_block_begin: Map[Symbol.Symbol, Operator] =
     Map(
       Symbol.bsub -> sub, Symbol.bsub_decoded -> sub,
       Symbol.bsup -> sup, Symbol.bsup_decoded -> sup)
 
   private val control_block_end: Map[Symbol.Symbol, Operator] =
     Map(
       Symbol.esub -> sub, Symbol.esub_decoded -> sub,
       Symbol.esup -> sup, Symbol.esup_decoded -> sup)
 
   def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym)
 
   def is_control_block_begin(sym: Symbol.Symbol): Boolean = control_block_begin.isDefinedAt(sym)
   def is_control_block_end(sym: Symbol.Symbol): Boolean = control_block_end.isDefinedAt(sym)
   def is_control_block_pair(bg: Symbol.Symbol, en: Symbol.Symbol): Boolean =
   {
     val bg_decoded = Symbol.decode(bg)
     val en_decoded = Symbol.decode(en)
     bg_decoded == Symbol.bsub_decoded && en_decoded == Symbol.esub_decoded ||
     bg_decoded == Symbol.bsup_decoded && en_decoded == Symbol.esup_decoded
   }
 
   def check_control_blocks(body: XML.Body): Boolean =
   {
     var ok = true
     var open = List.empty[Symbol.Symbol]
     for { XML.Text(text) <- body; sym <- Symbol.iterator(text) } {
       if (is_control_block_begin(sym)) open ::= sym
       else if (is_control_block_end(sym)) {
         open match {
           case bg :: rest if is_control_block_pair(bg, sym) => open = rest
           case _ => ok = false
         }
       }
     }
     ok && open.isEmpty
   }
 
   def output(s: StringBuilder, text: String,
     control_blocks: Boolean, hidden: Boolean, permissive: Boolean): Unit =
   {
     def output_string(str: String): Unit =
       XML.output_string(s, str, permissive = permissive)
 
     def output_hidden(body: => Unit): Unit =
       if (hidden) { s ++= "<span class=\"hidden\">"; body; s ++= "</span>" }
 
     def output_symbol(sym: Symbol.Symbol): Unit =
       if (sym != "") {
         control_block_begin.get(sym) match {
           case Some(op) if control_blocks =>
             output_hidden(output_string(sym))
             XML.output_elem(s, Markup(op.name, Nil))
           case _ =>
             control_block_end.get(sym) match {
               case Some(op) if control_blocks =>
                 XML.output_elem_end(s, op.name)
                 output_hidden(output_string(sym))
               case _ =>
                 if (hidden && Symbol.is_control_encoded(sym)) {
                   output_hidden(output_string(Symbol.control_prefix))
                   s ++= "<span class=\"control\">"
                   output_string(Symbol.control_name(sym).get)
                   s ++= "</span>"
                   output_hidden(output_string(Symbol.control_suffix))
                 }
                 else output_string(sym)
             }
         }
       }
 
     var ctrl = ""
     for (sym <- Symbol.iterator(text)) {
       if (is_control(sym)) { output_symbol(ctrl); ctrl = sym }
       else {
         control.get(ctrl) match {
           case Some(op) if Symbol.is_controllable(sym) =>
             output_hidden(output_symbol(ctrl))
             XML.output_elem(s, Markup(op.name, Nil))
             output_symbol(sym)
             XML.output_elem_end(s, op.name)
           case _ =>
             output_symbol(ctrl)
             output_symbol(sym)
         }
         ctrl = ""
       }
     }
     output_symbol(ctrl)
   }
 
   def output(text: String): String =
   {
     val control_blocks = check_control_blocks(List(XML.Text(text)))
     Library.make_string(output(_, text,
       control_blocks = control_blocks, hidden = false, permissive = true))
   }
 
 
   /* output XML as HTML */
 
   private val structural_elements =
     Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6",
       "ul", "ol", "dl", "li", "dt", "dd")
 
   def output(s: StringBuilder, xml: XML.Body, hidden: Boolean, structural: Boolean): Unit =
   {
     def output_body(body: XML.Body): Unit =
     {
       val control_blocks = check_control_blocks(body)
       body foreach {
         case XML.Elem(markup, Nil) =>
           XML.output_elem(s, markup, end = true)
         case XML.Elem(markup, ts) =>
           if (structural && structural_elements(markup.name)) s += '\n'
           XML.output_elem(s, markup)
           output_body(ts)
           XML.output_elem_end(s, markup.name)
           if (structural && structural_elements(markup.name)) s += '\n'
         case XML.Text(txt) =>
           output(s, txt, control_blocks = control_blocks, hidden = hidden, permissive = true)
       }
     }
     output_body(xml)
   }
 
   def output(body: XML.Body, hidden: Boolean, structural: Boolean): String =
     Library.make_string(output(_, body, hidden, structural))
 
   def output(tree: XML.Tree, hidden: Boolean, structural: Boolean): String =
     output(List(tree), hidden, structural)
 
 
   /* messages */
 
   // background
   val writeln_message: Attribute = class_("writeln_message")
   val warning_message: Attribute = class_("warning_message")
   val error_message: Attribute = class_("error_message")
 
   // underline
   val writeln: Attribute = class_("writeln")
   val warning: Attribute = class_("warning")
   val error: Attribute = class_("error")
 
 
   /* tooltips */
 
   def tooltip(item: XML.Body, tip: XML.Body): XML.Elem =
     span(item ::: List(div("tooltip", tip)))
 
   def tooltip_errors(item: XML.Body, msgs: List[XML.Body]): XML.Elem =
     HTML.error(tooltip(item, msgs.map(msg => error_message(pre(msg)))))
 
 
   /* GUI elements */
 
   object GUI
   {
     private def optional_value(text: String): XML.Attributes =
       proper_string(text).map(a => "value" -> a).toList
 
     private def optional_name(name: String): XML.Attributes =
       proper_string(name).map(a => "name" -> a).toList
 
     private def optional_title(tooltip: String): XML.Attributes =
       proper_string(tooltip).map(a => "title" -> a).toList
 
     private def optional_submit(submit: Boolean): XML.Attributes =
       if (submit) List("onChange" -> "this.form.submit()") else Nil
 
     private def optional_checked(selected: Boolean): XML.Attributes =
       if (selected) List("checked" -> "") else Nil
 
     private def optional_action(action: String): XML.Attributes =
       proper_string(action).map(a => "action" -> a).toList
 
     private def optional_onclick(script: String): XML.Attributes =
       proper_string(script).map(a => "onclick" -> a).toList
 
     private def optional_onchange(script: String): XML.Attributes =
       proper_string(script).map(a => "onchange" -> a).toList
 
     def button(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false,
         script: String = ""): XML.Elem =
       XML.Elem(
         Markup("button",
           List("type" -> (if (submit) "submit" else "button"), "value" -> "true") :::
           optional_name(name) ::: optional_title(tooltip) ::: optional_onclick(script)), body)
 
     def checkbox(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false,
         selected: Boolean = false, script: String = ""): XML.Elem =
       XML.elem("label",
         XML.elem(
           Markup("input",
             List("type" -> "checkbox", "value" -> "true") ::: optional_name(name) :::
               optional_title(tooltip) ::: optional_submit(submit) :::
               optional_checked(selected) ::: optional_onchange(script))) :: body)
 
     def text_field(columns: Int = 0, text: String = "", name: String = "", tooltip: String = "",
         submit: Boolean = false, script: String = ""): XML.Elem =
       XML.elem(Markup("input",
         List("type" -> "text") :::
           (if (columns > 0) List("size" -> columns.toString) else Nil) :::
           optional_value(text) ::: optional_name(name) ::: optional_title(tooltip) :::
           optional_submit(submit) ::: optional_onchange(script)))
 
     def parameter(text: String = "", name: String = ""): XML.Elem =
       XML.elem(
         Markup("input", List("type" -> "hidden") ::: optional_value(text) ::: optional_name(name)))
 
     def form(body: XML.Body, name: String = "", action: String = "", http_post: Boolean = false)
         : XML.Elem =
       XML.Elem(
         Markup("form", optional_name(name) ::: optional_action(action) :::
           (if (http_post) List("method" -> "post") else Nil)), body)
   }
 
 
   /* GUI layout */
 
   object Wrap_Panel
   {
     object Alignment extends Enumeration
     {
       val left, right, center = Value
     }
 
     def apply(contents: List[XML.Elem], name: String = "", action: String = "",
       alignment: Alignment.Value = Alignment.right): XML.Elem =
     {
       val body = Library.separate(XML.Text(" "), contents)
       GUI.form(List(div(body) + ("style" -> ("text-align: " + alignment))),
         name = name, action = action)
     }
   }
 
 
   /* document */
 
   val header: String =
     XML.header +
     """<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
 <html xmlns="http://www.w3.org/1999/xhtml">"""
 
   val footer: String = """</html>"""
 
   val head_meta: XML.Elem =
     XML.Elem(Markup("meta",
       List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil)
 
   def output_document(head: XML.Body, body: XML.Body,
     css: String = "isabelle.css",
     hidden: Boolean = true,
     structural: Boolean = true): String =
   {
     cat_lines(
       List(
         header,
         output(
           XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head),
           hidden = hidden, structural = structural),
         output(XML.elem("body", body),
           hidden = hidden, structural = structural),
         footer))
   }
 
 
   /* fonts */
 
   val fonts_path: Path = Path.explode("fonts")
 
   def init_fonts(dir: Path): Unit =
   {
     val fonts_dir = Isabelle_System.make_directory(dir + HTML.fonts_path)
     for (entry <- Isabelle_Fonts.fonts(hidden = true))
       Isabelle_System.copy_file(entry.path, fonts_dir)
   }
 
   def fonts_dir(prefix: String)(ttf_name: String): String = prefix + "/" + ttf_name
 
   def fonts_url(): String => String =
     (for (entry <- Isabelle_Fonts.fonts(hidden = true))
      yield (entry.path.file_name -> Url.print_file(entry.path.file))).toMap
 
   def fonts_css(make_url: String => String = fonts_url()): String =
   {
     def font_face(entry: Isabelle_Fonts.Entry): String =
       cat_lines(
         List(
           "@font-face {",
           "  font-family: '" + entry.family + "';",
           "  src: url('" + make_url(entry.path.file_name) + "') format('truetype');") :::
         (if (entry.is_bold) List("  font-weight: bold;") else Nil) :::
         (if (entry.is_italic) List("  font-style: italic;") else Nil) :::
         List("}"))
 
     ("/* Isabelle fonts */" :: Isabelle_Fonts.fonts(hidden = true).map(font_face))
       .mkString("", "\n\n", "\n")
   }
 
   def fonts_css_dir(prefix: String = ""): String =
   {
     val prefix1 = if (prefix.isEmpty || prefix.endsWith("/")) prefix else prefix + "/"
     fonts_css(fonts_dir(prefix1 + fonts_path.implode))
   }
 
 
   /* document directory context (fonts + css) */
 
   def relative_prefix(dir: Path, base: Option[Path]): String =
     base match {
       case None => ""
       case Some(base_dir) =>
-        File.path(dir.absolute.java_path.relativize(base_dir.absolute.java_path).toFile).implode
+        val path = File.path(dir.absolute.java_path.relativize(base_dir.absolute.java_path).toFile)
+        if (path.is_current) "" else path.implode + "/"
     }
 
   def isabelle_css: Path = Path.explode("~~/etc/isabelle.css")
 
   def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
     base: Option[Path] = None,
     css: String = isabelle_css.file_name,
     hidden: Boolean = true,
     structural: Boolean = true): Unit =
   {
     Isabelle_System.make_directory(dir)
     val prefix = relative_prefix(dir, base)
     File.write(dir + isabelle_css.base, fonts_css_dir(prefix) + "\n\n" + File.read(isabelle_css))
     File.write(dir + Path.basic(name),
       output_document(head, body, css = css, hidden = hidden, structural = structural))
   }
 }
diff --git a/src/Pure/Thy/presentation.scala b/src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala
+++ b/src/Pure/Thy/presentation.scala
@@ -1,623 +1,636 @@
 /*  Title:      Pure/Thy/presentation.scala
     Author:     Makarius
 
 HTML presentation of PIDE document content.
 */
 
 package isabelle
 
 
 import scala.annotation.tailrec
 import scala.collection.immutable.SortedMap
 import scala.collection.mutable
 
 
 object Presentation
 {
   /** HTML documents **/
 
   /* HTML context */
 
   sealed case class HTML_Document(title: String, content: String)
 
   def html_context(cache: Term.Cache = Term.Cache.make()): HTML_Context =
     new HTML_Context(cache)
 
   final class HTML_Context private[Presentation](val cache: Term.Cache)
   {
     private val already_presented = Synchronized(Set.empty[String])
     def register_presented(nodes: List[Document.Node.Name]): List[Document.Node.Name] =
       already_presented.change_result(presented =>
         (nodes.filterNot(name => presented.contains(name.theory)),
           presented ++ nodes.iterator.map(_.theory)))
 
     private val theory_cache = Synchronized(Map.empty[String, Export_Theory.Theory])
     def cache_theory(thy_name: String, make_thy: => Export_Theory.Theory): Export_Theory.Theory =
     {
       theory_cache.change_result(thys =>
       {
         thys.get(thy_name) match {
           case Some(thy) => (thy, thys)
           case None =>
             val thy = make_thy
             (thy, thys + (thy_name -> thy))
         }
       })
     }
 
     def head(title: String, rest: XML.Body = Nil): XML.Tree =
       HTML.div("head", HTML.chapter(title) :: rest)
 
     def source(body: XML.Body): XML.Tree = HTML.pre("source", body)
 
-    def physical_ref(range: Text.Range): String =
-      "offset_" + range.start + ".." + range.stop
-
     def contents(heading: String, items: List[XML.Body], css_class: String = "contents")
       : List[XML.Elem] =
     {
       if (items.isEmpty) Nil
       else List(HTML.div(css_class, List(HTML.section(heading), HTML.itemize(items))))
     }
 
     def html_document(title: String, body: XML.Body, fonts_css: String): HTML_Document =
     {
       val content =
         HTML.output_document(
           List(
             HTML.style(fonts_css + "\n\n" + File.read(HTML.isabelle_css)),
             HTML.title(title)),
           List(HTML.source(body)), css = "", structural = false)
       HTML_Document(title, content)
     }
   }
 
 
   /* presentation elements */
 
   sealed case class Elements(
     html: Markup.Elements = Markup.Elements.empty,
     entity: Markup.Elements = Markup.Elements.empty,
     language: Markup.Elements = Markup.Elements.empty)
 
   val elements1: Elements =
     Elements(
       html = Rendering.foreground_elements ++ Rendering.text_color_elements +
         Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE,
       entity = Markup.Elements(Markup.THEORY, Markup.TYPE_NAME, Markup.CONSTANT, Markup.FACT,
         Markup.CLASS, Markup.LOCALE, Markup.FREE))
 
   val elements2: Elements =
     Elements(
       html = elements1.html ++ Rendering.markdown_elements,
       language = Markup.Elements(Markup.Language.DOCUMENT))
 
 
   /* formal entities */
 
   type Entity = Export_Theory.Entity[Export_Theory.No_Content]
 
-  case class Entity_Context(node: Document.Node.Name)
+  object Entity_Context
   {
-    val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty
+    val empty: Entity_Context = new Entity_Context
+
+    def make(
+        session: String,
+        deps: Sessions.Deps,
+        node: Document.Node.Name,
+        theory_exports: Map[String, Export_Theory.Theory]): Entity_Context =
+      new Entity_Context {
+        private val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty
+
+        override def make_def(range: Symbol.Range, body: XML.Body): Option[XML.Elem] =
+        {
+          body match {
+            case List(XML.Elem(Markup("span", List("id" -> _)), _)) => None
+            case _ =>
+              Some {
+                val entities =
+                  theory_exports.get(node.theory).flatMap(_.entity_by_range.get(range))
+                    .getOrElse(Nil)
+                val body1 =
+                  if (seen_ranges.contains(range)) {
+                    HTML.entity_def(HTML.span(HTML.id(offset_id(range)), body))
+                  }
+                  else HTML.span(body)
+                entities.map(_.kname).foldLeft(body1) {
+                  case (elem, id) => HTML.entity_def(HTML.span(HTML.id(id), List(elem)))
+                }
+              }
+          }
+        }
+
+        private def offset_id(range: Text.Range): String =
+          "offset_" + range.start + ".." + range.stop
+
+        private def physical_ref(thy_name: String, props: Properties.T): Option[String] =
+        {
+          for {
+            range <- Position.Def_Range.unapply(props)
+            if thy_name == node.theory
+          } yield {
+            seen_ranges += range
+            offset_id(range)
+          }
+        }
+
+        private def logical_ref(thy_name: String, kind: String, name: String): Option[String] =
+          for {
+            thy <- theory_exports.get(thy_name)
+            entity <- thy.entity_by_kind_name.get((kind, name))
+          } yield entity.kname
+
+        override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
+        {
+          (props, props, props, props, props) match {
+            case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file), _, _) =>
+              val node_name = Resources.file_node(Path.explode(thy_file), theory = theory)
+              node_relative(deps, session, node_name).map(html_dir =>
+                HTML.link(html_dir + html_name(node_name), body))
+            case (Markup.Ref(_), Position.Def_File(def_file), Position.Def_Theory(def_theory),
+                Markup.Kind(kind), Markup.Name(name)) =>
+              val file_path = Path.explode(def_file)
+              val proper_thy_name =
+                proper_string(def_theory) orElse
+                  (if (File.eq(node.path, file_path)) Some(node.theory) else None)
+              for {
+                thy_name <- proper_thy_name
+                node_name = Resources.file_node(file_path, theory = thy_name)
+                html_dir <- node_relative(deps, session, node_name)
+                html_file = node_file(node_name)
+                html_ref <-
+                  logical_ref(thy_name, kind, name) orElse physical_ref(thy_name, props)
+              } yield {
+                HTML.entity_ref(HTML.link(html_dir + html_file + "#" + html_ref, body))
+              }
+            case _ => None
+          }
+        }
+      }
+  }
+
+  class Entity_Context
+  {
+    def make_def(range: Symbol.Range, body: XML.Body): Option[XML.Elem] = None
+    def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] = None
   }
 
 
   /* HTML output */
 
   private val div_elements =
     Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
       HTML.descr.name)
 
   def make_html(
-    name: Document.Node.Name,
+    entity_context: Entity_Context,
     elements: Elements,
-    entity_anchor: (Entity_Context, Symbol.Range, XML.Body) => Option[XML.Tree],
-    entity_link: (Entity_Context, Properties.T, XML.Body) => Option[XML.Tree],
     xml: XML.Body): XML.Body =
   {
-    val context = Entity_Context(name)
-
     def html_div(html: XML.Body): Boolean =
       html exists {
         case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body)
         case XML.Text(_) => false
       }
 
     def html_class(c: String, html: XML.Body): XML.Body =
       if (c == "") html
       else if (html_div(html)) List(HTML.div(c, html))
       else List(HTML.span(c, html))
 
     def html_body(xml_body: XML.Body, end_offset: Symbol.Offset): (XML.Body, Symbol.Offset) =
       xml_body.foldRight((List.empty[XML.Tree], end_offset)) { case (tree, (res, end_offset1)) =>
         val (res1, offset) = html_body_single(tree, end_offset1)
         (res1 ++ res, offset)
       }
 
     @tailrec
     def html_body_single(xml_tree: XML.Tree, end_offset: Symbol.Offset): (XML.Body, Symbol.Offset) =
       xml_tree match {
         case XML.Wrapped_Elem(markup, _, body) => html_body_single(XML.Elem(markup, body), end_offset)
         case XML.Elem(Markup(Markup.ENTITY, props @ Markup.Kind(kind)), body) =>
           val (body1, offset) = html_body(body, end_offset)
           if (elements.entity(kind)) {
-            entity_link(context, props, body1) match {
+            entity_context.make_ref(props, body1) match {
               case Some(link) => (List(link), offset)
               case None => (body1, offset)
             }
           }
           else (body1, offset)
         case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(name)), body) =>
           val (body1, offset) = html_body(body, end_offset)
           (html_class(if (elements.language(name)) name else "", body1), offset)
         case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) =>
           val (body1, offset) = html_body(body, end_offset)
           (List(HTML.par(body1)), offset)
         case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) =>
           val (body1, offset) = html_body(body, end_offset)
           (List(HTML.item(body1)), offset)
         case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), text) =>
           (Nil, end_offset - XML.symbol_length(text))
         case XML.Elem(Markup.Markdown_List(kind), body) =>
           val (body1, offset) = html_body(body, end_offset)
           if (kind == Markup.ENUMERATE) (List(HTML.enum(body1)), offset)
           else (List(HTML.list(body1)), offset)
         case XML.Elem(markup, body) =>
           val name = markup.name
           val (body1, offset) = html_body(body, end_offset)
           val html =
             markup.properties match {
               case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
                 html_class(kind, body1)
               case _ =>
                 body1
             }
           Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
             case Some(c) => (html_class(c.toString, html), offset)
             case None => (html_class(name, html), offset)
           }
         case XML.Text(text) =>
           val offset = end_offset - Symbol.length(text)
           val body = HTML.text(Symbol.decode(text))
-          entity_anchor(context, Text.Range(offset, end_offset), body) match {
+          entity_context.make_def(Text.Range(offset, end_offset), body) match {
             case Some(body1) => (List(body1), offset)
             case None => (body, offset)
           }
       }
 
     html_body(xml, XML.symbol_length(xml) + 1)._1
   }
 
 
   /* PIDE HTML document */
 
   def html_document(
-    resources: Resources,
     snapshot: Document.Snapshot,
     html_context: HTML_Context,
     elements: Elements,
     plain_text: Boolean = false,
     fonts_css: String = HTML.fonts_css()): HTML_Document =
   {
     require(!snapshot.is_outdated, "document snapshot outdated")
 
     val name = snapshot.node_name
     if (plain_text) {
       val title = "File " + Symbol.cartouche_decoded(name.path.file_name)
       val body = HTML.text(snapshot.node.source)
       html_context.html_document(title, body, fonts_css)
     }
     else {
-      resources.html_document(snapshot) getOrElse {
+      Resources.html_document(snapshot) getOrElse {
         val title =
           if (name.is_theory) "Theory " + quote(name.theory_base_name)
           else "File " + Symbol.cartouche_decoded(name.path.file_name)
         val xml = snapshot.xml_markup(elements = elements.html)
-        val body = make_html(name, elements, (_, _, _) => None, (_, _, _) => None, xml)
+        val body = make_html(Entity_Context.empty, elements, xml)
         html_context.html_document(title, body, fonts_css)
       }
     }
   }
 
 
 
   /** HTML presentation **/
 
   /* presentation context */
 
   object Context
   {
     val none: Context = new Context { def enabled: Boolean = false }
     val standard: Context = new Context { def enabled: Boolean = true }
 
     def dir(path: Path): Context =
       new Context {
         def enabled: Boolean = true
         override def dir(store: Sessions.Store): Path = path
       }
 
     def make(s: String): Context =
       if (s == ":") standard else dir(Path.explode(s))
   }
 
   abstract class Context private
   {
     def enabled: Boolean
     def enabled(info: Sessions.Info): Boolean = enabled || info.browser_info
     def dir(store: Sessions.Store): Path = store.presentation_dir
     def dir(store: Sessions.Store, info: Sessions.Info): Path =
       dir(store) + Path.explode(info.chapter_session)
   }
 
 
   /* maintain chapter index */
 
   private val sessions_path = Path.basic(".sessions")
 
   private def read_sessions(dir: Path): List[(String, String)] =
   {
     val path = dir + sessions_path
     if (path.is_file) {
       import XML.Decode._
       list(pair(string, string))(Symbol.decode_yxml(File.read(path)))
     }
     else Nil
   }
 
   def update_chapter(
     presentation_dir: Path, chapter: String, new_sessions: List[(String, String)]): Unit =
   {
     val dir = Isabelle_System.make_directory(presentation_dir + Path.basic(chapter))
 
     val sessions0 =
       try { read_sessions(dir) }
       catch { case _: XML.Error => Nil }
 
     val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
     File.write(dir + sessions_path,
       {
         import XML.Encode._
         YXML.string_of_body(list(pair(string, string))(sessions))
       })
 
     val title = "Isabelle/" + chapter + " sessions"
     HTML.write_document(dir, "index.html",
       List(HTML.title(title + Isabelle_System.isabelle_heading())),
       HTML.chapter(title) ::
        (if (sessions.isEmpty) Nil
         else
           List(HTML.div("sessions",
             List(HTML.description(
               sessions.map({ case (name, description) =>
                 val descr = Symbol.trim_blank_lines(description)
                 (List(HTML.link(name + "/index.html", HTML.text(name))),
                   if (descr == "") Nil
                   else HTML.break ::: List(HTML.pre(HTML.text(descr)))) })))))),
       base = Some(presentation_dir))
   }
 
   def update_root(presentation_dir: Path): Unit =
   {
     Isabelle_System.make_directory(presentation_dir)
     HTML.init_fonts(presentation_dir)
     Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"),
       presentation_dir + Path.explode("isabelle.gif"))
     val title = "The " + XML.text(Isabelle_System.isabelle_name()) + " Library"
     File.write(presentation_dir + Path.explode("index.html"),
       HTML.header +
 """
 <head>
   """ + HTML.head_meta + """
   <title>""" + title + """</title>
 </head>
 
 <body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040">
   <center>
     <table width="100%" border="0" cellspacing="10" cellpadding="0">
       <tr>
         <td width="20%" valign="middle" align="center"><a href="https://isabelle.in.tum.de/"><img align="bottom" src="isabelle.gif" width="100" height="86" alt="[Isabelle]" border="0" /></a></td>
 
         <td width="80%" valign="middle" align="center">
           <table width="90%" border="0" cellspacing="0" cellpadding="20">
             <tr>
               <td valign="middle" align="center" bgcolor="#AACCCC"><font face="Helvetica,Arial" size="+2">""" + title + """</font></td>
             </tr>
           </table>
         </td>
       </tr>
     </table>
   </center>
   <hr />
 """ + File.read(Path.explode("~~/lib/html/library_index_content.template")) +
 """
 </body>
 """ + HTML.footer)
   }
 
 
   /* present session */
 
   val session_graph_path = Path.explode("session_graph.pdf")
   val readme_path = Path.explode("README.html")
   val files_path = Path.explode("files")
 
   def html_name(name: Document.Node.Name): String = Path.explode(name.theory_base_name).html.implode
   def html_path(path: Path): String = (files_path + path.squash.html).implode
 
-  def session_relative(deps: Sessions.Deps, session0: String, session1: String): Option[String] =
+  private def node_file(node: Document.Node.Name): String =
+    if (node.node.endsWith(".thy")) html_name(node) else html_path(Path.explode(node.node))
+
+  private def session_relative(deps: Sessions.Deps, session0: String, session1: String): Option[String] =
   {
     for {
       info0 <- deps.sessions_structure.get(session0)
       info1 <- deps.sessions_structure.get(session1)
     } yield info0.relative_path(info1)
   }
 
   def node_relative(
     deps: Sessions.Deps,
     session0: String,
     node_name: Document.Node.Name): Option[String] =
   {
     val session1 = deps(session0).theory_qualifier(node_name)
     session_relative(deps, session0, session1)
   }
 
   def theory_link(deps: Sessions.Deps, session0: String,
     name: Document.Node.Name, body: XML.Body, anchor: Option[String] = None): Option[XML.Tree] =
   {
     val session1 = deps(session0).theory_qualifier(name)
     val info0 = deps.sessions_structure.get(session0)
     val info1 = deps.sessions_structure.get(session1)
     val fragment = if (anchor.isDefined) "#" + anchor.get else ""
     if (info0.isDefined && info1.isDefined) {
       Some(HTML.link(info0.get.relative_path(info1.get) + html_name(name) + fragment, body))
     }
     else None
   }
 
   def session_html(
-    resources: Resources,
     session: String,
     deps: Sessions.Deps,
     db_context: Sessions.Database_Context,
     progress: Progress = new Progress,
     verbose: Boolean = false,
     html_context: HTML_Context,
     session_elements: Elements,
     presentation: Context): Unit =
   {
     val hierarchy = deps.sessions_structure.hierarchy(session)
     val info = deps.sessions_structure(session)
     val options = info.options
     val base = deps(session)
 
     def make_session_dir(name: String): Path =
       Isabelle_System.make_directory(
         presentation.dir(db_context.store, deps.sessions_structure(name)))
 
     val session_dir = make_session_dir(session)
     val presentation_dir = presentation.dir(db_context.store)
 
     Bytes.write(session_dir + session_graph_path,
       graphview.Graph_File.make_pdf(options, base.session_graph_display))
 
     val documents =
       for {
         doc <- info.document_variants
         document <- db_context.input_database(session)(Document_Build.read_document(_, _, doc.name))
       } yield {
         val doc_path = (session_dir + doc.path.pdf).expand
         if (verbose) progress.echo("Presenting document " + session + "/" + doc.name)
         if (options.bool("document_echo")) progress.echo("Document at " + doc_path)
         Bytes.write(doc_path, document.pdf)
         doc
       }
 
     val view_links =
     {
       val deps_link =
         HTML.link(session_graph_path, HTML.text("theory dependencies"))
 
       val readme_links =
         if ((info.dir + readme_path).is_file) {
           Isabelle_System.copy_file(info.dir + readme_path, session_dir + readme_path)
           List(HTML.link(readme_path, HTML.text("README")))
         }
         else Nil
 
       val document_links =
         documents.map(doc => HTML.link(doc.path.pdf, HTML.text(doc.name)))
 
       Library.separate(HTML.break ::: HTML.nl,
         (deps_link :: readme_links ::: document_links).
           map(link => HTML.text("View ") ::: List(link))).flatten
     }
 
     val all_used_theories = hierarchy.reverse.flatMap(a => deps(a).used_theories.map(_._1))
     val present_theories = html_context.register_presented(all_used_theories)
 
     val theory_exports: Map[String, Export_Theory.Theory] =
       (for (node <- all_used_theories.iterator) yield {
         val thy_name = node.theory
         val theory =
           if (thy_name == Thy_Header.PURE) Export_Theory.no_theory
           else {
             html_context.cache_theory(thy_name,
               {
                 val provider = Export.Provider.database_context(db_context, hierarchy, thy_name)
                 if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) {
                   Export_Theory.read_theory(
                     provider, session, thy_name, cache = html_context.cache)
                 }
                 else Export_Theory.no_theory
               })
         }
         thy_name -> theory
       }).toMap
 
+    def entity_context(name: Document.Node.Name): Entity_Context =
+      Entity_Context.make(session, deps, name, theory_exports)
+
     val theories: List[XML.Body] =
     {
       sealed case class Seen_File(
         src_path: Path, file_name: String, thy_session: String, thy_name: Document.Node.Name)
       {
         def check(src_path1: Path, file_name1: String, thy_session1: String): Boolean =
           (src_path == src_path1 || file_name == file_name1) && thy_session == thy_session1
       }
       var seen_files = List.empty[Seen_File]
 
-      def node_file(node: Document.Node.Name): String =
-        if (node.node.endsWith(".thy")) html_name(node) else html_path(Path.explode(node.node))
-
-      def entity_anchor(
-        context: Entity_Context, range: Symbol.Range, body: XML.Body): Option[XML.Elem] =
-      {
-        body match {
-          case List(XML.Elem(Markup("span", List("id" -> _)), _)) => None
-          case _ =>
-            Some {
-              val entities =
-                theory_exports.get(context.node.theory).flatMap(_.entity_by_range.get(range))
-                  .getOrElse(Nil)
-              val body1 =
-                if (context.seen_ranges.contains(range)) {
-                  HTML.entity_def(HTML.span(HTML.id(html_context.physical_ref(range)), body))
-                }
-                else HTML.span(body)
-              entities.map(_.kname).foldLeft(body1) {
-                case (elem, id) => HTML.entity_def(HTML.span(HTML.id(id), List(elem)))
-              }
-            }
-        }
-      }
-
-      def logical_ref(thy_name: String, kind: String, name: String): Option[String] =
-        for {
-          thy <- theory_exports.get(thy_name)
-          entity <- thy.entity_by_kind_name.get((kind, name))
-        } yield entity.kname
-
-      def physical_ref(
-        context: Entity_Context, thy_name: String, props: Properties.T): Option[String] =
-      {
-        for {
-          range <- Position.Def_Range.unapply(props)
-          if thy_name == context.node.theory
-        } yield {
-          context.seen_ranges += range
-          html_context.physical_ref(range)
-        }
-      }
-
-      def entity_link(
-        context: Entity_Context, props: Properties.T, body: XML.Body): Option[XML.Elem] =
-      {
-        (props, props, props, props, props) match {
-          case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file), _, _) =>
-            val node_name = resources.file_node(Path.explode(thy_file), theory = theory)
-            node_relative(deps, session, node_name).map(html_dir =>
-              HTML.link(html_dir + html_name(node_name), body))
-          case (Markup.Ref(_), Position.Def_File(thy_file), Position.Def_Theory(def_theory),
-              Markup.Kind(kind), Markup.Name(name)) =>
-            val thy_name = if (def_theory.nonEmpty) def_theory else context.node.theory
-            val node_name = resources.file_node(Path.explode(thy_file), theory = thy_name)
-            for {
-              html_dir <- node_relative(deps, session, node_name)
-              html_file = node_file(node_name)
-              html_ref <-
-                logical_ref(thy_name, kind, name) orElse physical_ref(context, thy_name, props)
-            } yield {
-              HTML.entity_ref(HTML.link(html_dir + html_file + "#" + html_ref, body))
-            }
-          case _ => None
-        }
-      }
-
       sealed case class Theory(
         name: Document.Node.Name,
         command: Command,
         files_html: List[(Path, XML.Tree)],
         html: XML.Tree)
 
       def read_theory(name: Document.Node.Name): Option[Theory] =
       {
         progress.expose_interrupt()
 
-        for (command <- Build_Job.read_theory(db_context, resources, hierarchy, name.theory))
+        for (command <- Build_Job.read_theory(db_context, hierarchy, name.theory))
         yield {
           if (verbose) progress.echo("Presenting theory " + name)
           val snapshot = Document.State.init.snippet(command)
 
           val thy_elements =
             session_elements.copy(entity =
               theory_exports(name.theory).others.keySet.foldLeft(session_elements.entity)(_ + _))
 
           val files_html =
             for {
               (src_path, xml) <- snapshot.xml_markup_blobs(elements = thy_elements.html)
               if xml.nonEmpty
             }
             yield {
               progress.expose_interrupt()
               if (verbose) progress.echo("Presenting file " + src_path)
 
               (src_path, html_context.source(
-                make_html(name, thy_elements, entity_anchor, entity_link, xml)))
+                make_html(entity_context(name), thy_elements, xml)))
             }
 
           val html =
             html_context.source(
-              make_html(name, thy_elements, entity_anchor, entity_link,
+              make_html(entity_context(name), thy_elements,
                 snapshot.xml_markup(elements = thy_elements.html)))
 
           Theory(name, command, files_html, html)
         }
       }
 
       (for (thy <- Par_List.map(read_theory, present_theories).flatten) yield {
         val thy_session = base.theory_qualifier(thy.name)
         val thy_dir = make_session_dir(thy_session)
         val files =
           for { (src_path, file_html) <- thy.files_html }
           yield {
             val file_name = html_path(src_path)
 
             seen_files.find(_.check(src_path, file_name, thy_session)) match {
               case None => seen_files ::= Seen_File(src_path, file_name, thy_session, thy.name)
               case Some(seen_file) =>
                 error("Incoherent use of file name " + src_path + " as " + quote(file_name) +
                   " in theory " + seen_file.thy_name + " vs. " + thy.name)
             }
 
             val file_path = thy_dir + Path.explode(file_name)
             val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short)
             HTML.write_document(file_path.dir, file_path.file_name,
               List(HTML.title(file_title)), List(html_context.head(file_title), file_html),
               base = Some(presentation_dir))
 
             List(HTML.link(file_name, HTML.text(file_title)))
           }
 
         val thy_title = "Theory " + thy.name.theory_base_name
 
         HTML.write_document(thy_dir, html_name(thy.name),
           List(HTML.title(thy_title)), List(html_context.head(thy_title), thy.html),
           base = Some(presentation_dir))
 
         if (thy_session == session) {
           Some(
             List(HTML.link(html_name(thy.name),
               HTML.text(thy.name.theory_base_name) :::
                 (if (files.isEmpty) Nil else List(HTML.itemize(files))))))
         }
         else None
       }).flatten
     }
 
     val title = "Session " + session
     HTML.write_document(session_dir, "index.html",
       List(HTML.title(title + Isabelle_System.isabelle_heading())),
       html_context.head(title, List(HTML.par(view_links))) ::
         html_context.contents("Theories", theories),
       base = Some(presentation_dir))
   }
 }
diff --git a/src/Pure/Tools/build.scala b/src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala
+++ b/src/Pure/Tools/build.scala
@@ -1,685 +1,684 @@
 /*  Title:      Pure/Tools/build.scala
     Author:     Makarius
     Options:    :folding=explicit:
 
 Build and manage Isabelle sessions.
 */
 
 package isabelle
 
 
 import scala.collection.immutable.SortedSet
 import scala.annotation.tailrec
 
 
 object Build
 {
   /** auxiliary **/
 
   /* persistent build info */
 
   sealed case class Session_Info(
     sources: String,
     input_heaps: List[String],
     output_heap: Option[String],
     return_code: Int)
   {
     def ok: Boolean = return_code == 0
   }
 
 
   /* queue with scheduling information */
 
   private object Queue
   {
     type Timings = (List[Properties.T], Double)
 
     def load_timings(progress: Progress, store: Sessions.Store, session_name: String): Timings =
     {
       val no_timings: Timings = (Nil, 0.0)
 
       store.try_open_database(session_name) match {
         case None => no_timings
         case Some(db) =>
           def ignore_error(msg: String) =
           {
             progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg))
             no_timings
           }
           try {
             val command_timings = store.read_command_timings(db, session_name)
             val session_timing =
               store.read_session_timing(db, session_name) match {
                 case Markup.Elapsed(t) => t
                 case _ => 0.0
               }
             (command_timings, session_timing)
           }
           catch {
             case ERROR(msg) => ignore_error(msg)
             case exn: java.lang.Error => ignore_error(Exn.message(exn))
             case _: XML.Error => ignore_error("")
           }
           finally { db.close() }
       }
     }
 
     def make_session_timing(sessions_structure: Sessions.Structure, timing: Map[String, Double])
       : Map[String, Double] =
     {
       val maximals = sessions_structure.build_graph.maximals.toSet
       def desc_timing(session_name: String): Double =
       {
         if (maximals.contains(session_name)) timing(session_name)
         else {
           val descendants = sessions_structure.build_descendants(List(session_name)).toSet
           val g = sessions_structure.build_graph.restrict(descendants)
           (0.0 :: g.maximals.flatMap(desc => {
             val ps = g.all_preds(List(desc))
             if (ps.exists(p => !timing.isDefinedAt(p))) None
             else Some(ps.map(timing(_)).sum)
           })).max
         }
       }
       timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
     }
 
     def apply(progress: Progress, sessions_structure: Sessions.Structure, store: Sessions.Store)
       : Queue =
     {
       val graph = sessions_structure.build_graph
       val names = graph.keys
 
       val timings = names.map(name => (name, load_timings(progress, store, name)))
       val command_timings =
         timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
       val session_timing =
         make_session_timing(sessions_structure,
           timings.map({ case (name, (_, t)) => (name, t) }).toMap)
 
       object Ordering extends scala.math.Ordering[String]
       {
         def compare(name1: String, name2: String): Int =
           session_timing(name2) compare session_timing(name1) match {
             case 0 =>
               sessions_structure(name2).timeout compare sessions_structure(name1).timeout match {
                 case 0 => name1 compare name2
                 case ord => ord
               }
             case ord => ord
           }
       }
 
       new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
     }
   }
 
   private class Queue(
     graph: Graph[String, Sessions.Info],
     order: SortedSet[String],
     val command_timings: String => List[Properties.T])
   {
     def is_inner(name: String): Boolean = !graph.is_maximal(name)
 
     def is_empty: Boolean = graph.is_empty
 
     def - (name: String): Queue =
       new Queue(graph.del_node(name), order - name, command_timings)
 
     def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
     {
       val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
       if (it.hasNext) { val name = it.next(); Some((name, graph.get_node(name))) }
       else None
     }
   }
 
 
 
   /** build with results **/
 
   class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)])
   {
     def sessions: Set[String] = results.keySet
     def infos: List[Sessions.Info] = results.values.map(_._2).toList
     def cancelled(name: String): Boolean = results(name)._1.isEmpty
     def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
     def get_info(name: String): Option[Sessions.Info] = results.get(name).map(_._2)
     def info(name: String): Sessions.Info = get_info(name).get
     val rc: Int =
       results.iterator.map({ case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }).
         foldLeft(Process_Result.RC.ok)(_ max _)
     def ok: Boolean = rc == Process_Result.RC.ok
 
     override def toString: String = rc.toString
   }
 
   def session_finished(session_name: String, process_result: Process_Result): String =
     "Finished " + session_name + " (" + process_result.timing.message_resources + ")"
 
   def session_timing(session_name: String, build_log: Build_Log.Session_Info): String =
   {
     val props = build_log.session_timing
     val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1
     val timing = Markup.Timing_Properties.parse(props)
     "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
   }
 
   def build(
     options: Options,
     selection: Sessions.Selection = Sessions.Selection.empty,
     presentation: Presentation.Context = Presentation.Context.none,
     progress: Progress = new Progress,
     check_unknown_files: Boolean = false,
     build_heap: Boolean = false,
     clean_build: Boolean = false,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     infos: List[Sessions.Info] = Nil,
     numa_shuffling: Boolean = false,
     max_jobs: Int = 1,
     list_files: Boolean = false,
     check_keywords: Set[String] = Set.empty,
     fresh_build: Boolean = false,
     no_build: Boolean = false,
     soft_build: Boolean = false,
     verbose: Boolean = false,
     export_files: Boolean = false,
     session_setup: (String, Session) => Unit = (_, _) => ()): Results =
   {
     val build_options =
       options +
         "completion_limit=0" +
         "editor_tracing_messages=0" +
         "kodkod_scala=false" +
         ("pide_reports=" + options.bool("build_pide_reports"))
 
     val store = Sessions.store(build_options)
 
     Isabelle_Fonts.init()
 
 
     /* session selection and dependencies */
 
     val full_sessions =
       Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
 
     val full_sessions_selection = full_sessions.imports_selection(selection)
 
     def sources_stamp(deps: Sessions.Deps, session_name: String): String =
     {
       val digests =
         full_sessions(session_name).meta_digest ::
         deps.sources(session_name) :::
         deps.imported_sources(session_name)
       SHA1.digest_set(digests).toString
     }
 
     val deps =
     {
       val deps0 =
         Sessions.deps(full_sessions.selection(selection),
           progress = progress, inlined_files = true, verbose = verbose,
           list_files = list_files, check_keywords = check_keywords).check_errors
 
       if (soft_build && !fresh_build) {
         val outdated =
           deps0.sessions_structure.build_topological_order.flatMap(name =>
             store.try_open_database(name) match {
               case Some(db) =>
                 using(db)(store.read_build(_, name)) match {
                   case Some(build)
                   if build.ok && build.sources == sources_stamp(deps0, name) => None
                   case _ => Some(name)
                 }
               case None => Some(name)
             })
 
         Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)),
           progress = progress, inlined_files = true).check_errors
       }
       else deps0
     }
 
 
     /* check unknown files */
 
     if (check_unknown_files) {
       val source_files =
         (for {
           (_, base) <- deps.session_bases.iterator
           (path, _) <- base.sources.iterator
         } yield path).toList
       val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
       val unknown_files =
         Mercurial.check_files(source_files)._2.
           filterNot(path => exclude_files.contains(path.canonical_file))
       if (unknown_files.nonEmpty) {
         progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
           unknown_files.map(path => path.expand.implode).sorted.mkString("\n  ", "\n  ", ""))
       }
     }
 
 
     /* main build process */
 
     val queue = Queue(progress, deps.sessions_structure, store)
 
     store.prepare_output_dir()
 
     if (clean_build) {
       for (name <- full_sessions.imports_descendants(full_sessions_selection)) {
         val (relevant, ok) = store.clean_output(name)
         if (relevant) {
           if (ok) progress.echo("Cleaned " + name)
           else progress.echo(name + " FAILED to clean")
         }
       }
     }
 
     // scheduler loop
     case class Result(
       current: Boolean,
       heap_digest: Option[String],
       process: Option[Process_Result],
       info: Sessions.Info)
     {
       def ok: Boolean =
         process match {
           case None => false
           case Some(res) => res.ok
         }
     }
 
     def sleep(): Unit =
       Isabelle_Thread.interrupt_handler(_ => progress.stop()) { Time.seconds(0.5).sleep() }
 
     val log =
       build_options.string("system_log") match {
         case "" => No_Logger
         case "true" => Logger.make(progress)
         case log_file => Logger.make(Some(Path.explode(log_file)))
       }
 
     val numa_nodes = new NUMA.Nodes(numa_shuffling)
 
     @tailrec def loop(
       pending: Queue,
       running: Map[String, (List[String], Build_Job)],
       results: Map[String, Result]): Map[String, Result] =
     {
       def used_node(i: Int): Boolean =
         running.iterator.exists(
           { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
 
       if (pending.is_empty) results
       else {
         if (progress.stopped) {
           for ((_, (_, job)) <- running) job.terminate()
         }
 
         running.find({ case (_, (_, job)) => job.is_finished }) match {
           case Some((session_name, (input_heaps, job))) =>
             //{{{ finish job
 
             val (process_result, heap_digest) = job.join
 
             val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
             val process_result_tail =
             {
               val tail = job.info.options.int("process_output_tail")
               process_result.copy(
                 out_lines =
                   "(see also " + store.output_log(session_name).file.toString + ")" ::
                   (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
             }
 
             val build_log =
               Build_Log.Log_File(session_name, process_result.out_lines).
                 parse_session_info(
                   command_timings = true,
                   theory_timings = true,
                   ml_statistics = true,
                   task_statistics = true)
 
             // write log file
             if (process_result.ok) {
               File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines))
             }
             else File.write(store.output_log(session_name), terminate_lines(log_lines))
 
             // write database
             using(store.open_database(session_name, output = true))(db =>
               store.write_session_info(db, session_name,
                 build_log =
                   if (process_result.timeout) build_log.error("Timeout") else build_log,
                 build =
                   Session_Info(sources_stamp(deps, session_name), input_heaps, heap_digest,
                     process_result.rc)))
 
             // messages
             process_result.err_lines.foreach(progress.echo)
 
             if (process_result.ok) {
               if (verbose) progress.echo(session_timing(session_name, build_log))
               progress.echo(session_finished(session_name, process_result))
             }
             else {
               progress.echo(session_name + " FAILED")
               if (!process_result.interrupted) progress.echo(process_result_tail.out)
             }
 
             loop(pending - session_name, running - session_name,
               results +
                 (session_name -> Result(false, heap_digest, Some(process_result_tail), job.info)))
             //}}}
           case None if running.size < (max_jobs max 1) =>
             //{{{ check/start next job
             pending.dequeue(running.isDefinedAt) match {
               case Some((session_name, info)) =>
                 val ancestor_results =
                   deps.sessions_structure.build_requirements(List(session_name)).
                     filterNot(_ == session_name).map(results(_))
                 val ancestor_heaps = ancestor_results.flatMap(_.heap_digest)
 
                 val do_store =
                   build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name)
 
                 val (current, heap_digest) =
                 {
                   store.try_open_database(session_name) match {
                     case Some(db) =>
                       using(db)(store.read_build(_, session_name)) match {
                         case Some(build) =>
                           val heap_digest = store.find_heap_digest(session_name)
                           val current =
                             !fresh_build &&
                             build.ok &&
                             build.sources == sources_stamp(deps, session_name) &&
                             build.input_heaps == ancestor_heaps &&
                             build.output_heap == heap_digest &&
                             !(do_store && heap_digest.isEmpty)
                           (current, heap_digest)
                         case None => (false, None)
                       }
                     case None => (false, None)
                   }
                 }
                 val all_current = current && ancestor_results.forall(_.current)
 
                 if (all_current)
                   loop(pending - session_name, running,
                     results +
                       (session_name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
                 else if (no_build) {
                   progress.echo_if(verbose, "Skipping " + session_name + " ...")
                   loop(pending - session_name, running,
                     results +
                       (session_name -> Result(false, heap_digest, Some(Process_Result(1)), info)))
                 }
                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
                   progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")
 
                   store.clean_output(session_name)
                   using(store.open_database(session_name, output = true))(
                     store.init_session_info(_, session_name))
 
                   val numa_node = numa_nodes.next(used_node)
                   val job =
                     new Build_Job(progress, session_name, info, deps, store, do_store,
                       log, session_setup, numa_node, queue.command_timings(session_name))
                   loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
                 }
                 else {
                   progress.echo(session_name + " CANCELLED")
                   loop(pending - session_name, running,
                     results + (session_name -> Result(false, heap_digest, None, info)))
                 }
               case None => sleep(); loop(pending, running, results)
             }
             ///}}}
           case None => sleep(); loop(pending, running, results)
         }
       }
     }
 
 
     /* build results */
 
     val results =
     {
       val results0 =
         if (deps.is_empty) {
           progress.echo_warning("Nothing to build")
           Map.empty[String, Result]
         }
         else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) }
 
       new Results(
         (for ((name, result) <- results0.iterator)
           yield (name, (result.process, result.info))).toMap)
     }
 
     if (export_files) {
       for (name <- full_sessions.imports_selection(selection).iterator if results(name).ok) {
         val info = results.info(name)
         if (info.export_files.nonEmpty) {
           progress.echo("Exporting " + info.name + " ...")
           for ((dir, prune, pats) <- info.export_files) {
             Export.export_files(store, name, info.dir + dir,
               progress = if (verbose) progress else new Progress,
               export_prune = prune,
               export_patterns = pats)
           }
         }
       }
     }
 
     if (results.rc != Process_Result.RC.ok && (verbose || !no_build)) {
       val unfinished =
         (for {
           name <- results.sessions.iterator
           if !results(name).ok
          } yield name).toList.sorted
       progress.echo("Unfinished session(s): " + commas(unfinished))
     }
 
 
     /* PDF/HTML presentation */
 
     if (!no_build && !progress.stopped && results.ok) {
       val selected = full_sessions_selection.toSet
       val presentation_sessions =
         (for {
           session_name <- deps.sessions_structure.imports_topological_order.iterator
           info <- results.get_info(session_name)
           if selected(session_name) && presentation.enabled(info) && results(session_name).ok }
         yield info).toList
 
       if (presentation_sessions.nonEmpty) {
         val presentation_dir = presentation.dir(store)
         progress.echo("Presentation in " + presentation_dir.absolute)
         Presentation.update_root(presentation_dir)
 
         for ((chapter, infos) <- presentation_sessions.groupBy(_.chapter).iterator) {
           val entries = infos.map(info => (info.name, info.description))
           Presentation.update_chapter(presentation_dir, chapter, entries)
         }
 
-        val resources = Resources.empty
         val html_context = Presentation.html_context(cache = store.cache)
 
         using(store.open_database_context())(db_context =>
           for (info <- presentation_sessions) {
             progress.expose_interrupt()
             progress.echo("Presenting " + info.name + " ...")
             Presentation.session_html(
-              resources, info.name, deps, db_context, progress = progress,
+              info.name, deps, db_context, progress = progress,
               verbose = verbose, html_context = html_context,
               Presentation.elements1, presentation = presentation)
           })
       }
     }
 
     results
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions",
     Scala_Project.here, args =>
   {
     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
 
     var base_sessions: List[String] = Nil
     var select_dirs: List[Path] = Nil
     var numa_shuffling = false
     var presentation = Presentation.Context.none
     var requirements = false
     var soft_build = false
     var exclude_session_groups: List[String] = Nil
     var all_sessions = false
     var build_heap = false
     var clean_build = false
     var dirs: List[Path] = Nil
     var export_files = false
     var fresh_build = false
     var session_groups: List[String] = Nil
     var max_jobs = 1
     var check_keywords: Set[String] = Set.empty
     var list_files = false
     var no_build = false
     var options = Options.init(opts = build_options)
     var verbose = false
     var exclude_sessions: List[String] = Nil
 
     val getopts = Getopts("""
 Usage: isabelle build [OPTIONS] [SESSIONS ...]
 
   Options are:
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -P DIR       enable HTML/PDF presentation in directory (":" for default)
     -R           refer to requirements of selected sessions
     -S           soft build: only observe changes of sources, not heap images
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
     -b           build heap images
     -c           clean build
     -d DIR       include session directory
     -e           export files from session specification into file-system
     -f           fresh build
     -g NAME      select session group NAME
     -j INT       maximum number of parallel jobs (default 1)
     -k KEYWORD   check theory sources for conflicts with proposed keywords
     -l           list session source files
     -n           no build -- test dependencies only
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           verbose
     -x NAME      exclude session NAME and all descendants
 
   Build and manage Isabelle sessions, depending on implicit settings:
 
 """ + Library.indent_lines(2,  Build_Log.Settings.show()) + "\n",
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "N" -> (_ => numa_shuffling = true),
       "P:" -> (arg => presentation = Presentation.Context.make(arg)),
       "R" -> (_ => requirements = true),
       "S" -> (_ => soft_build = true),
       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
       "a" -> (_ => all_sessions = true),
       "b" -> (_ => build_heap = true),
       "c" -> (_ => clean_build = true),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "e" -> (_ => export_files = true),
       "f" -> (_ => fresh_build = true),
       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
       "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
       "k:" -> (arg => check_keywords = check_keywords + arg),
       "l" -> (_ => list_files = true),
       "n" -> (_ => no_build = true),
       "o:" -> (arg => options = options + arg),
       "v" -> (_ => verbose = true),
       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
 
     val sessions = getopts(args)
 
     val progress = new Console_Progress(verbose = verbose)
 
     val start_date = Date.now()
 
     if (verbose) {
       progress.echo(
         "Started at " + Build_Log.print_date(start_date) +
           " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
       progress.echo(Build_Log.Settings.show() + "\n")
     }
 
     val results =
       progress.interrupt_handler {
         build(options,
           selection = Sessions.Selection(
             requirements = requirements,
             all_sessions = all_sessions,
             base_sessions = base_sessions,
             exclude_session_groups = exclude_session_groups,
             exclude_sessions = exclude_sessions,
             session_groups = session_groups,
             sessions = sessions),
           presentation = presentation,
           progress = progress,
           check_unknown_files = Mercurial.is_repository(Path.ISABELLE_HOME),
           build_heap = build_heap,
           clean_build = clean_build,
           dirs = dirs,
           select_dirs = select_dirs,
           numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
           max_jobs = max_jobs,
           list_files = list_files,
           check_keywords = check_keywords,
           fresh_build = fresh_build,
           no_build = no_build,
           soft_build = soft_build,
           verbose = verbose,
           export_files = export_files)
       }
     val end_date = Date.now()
     val elapsed_time = end_date.time - start_date.time
 
     if (verbose) {
       progress.echo("\nFinished at " + Build_Log.print_date(end_date))
     }
 
     val total_timing =
       results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
         copy(elapsed = elapsed_time)
     progress.echo(total_timing.message_resources)
 
     sys.exit(results.rc)
   })
 
 
   /* build logic image */
 
   def build_logic(options: Options, logic: String,
     progress: Progress = new Progress,
     build_heap: Boolean = false,
     dirs: List[Path] = Nil,
     fresh: Boolean = false,
     strict: Boolean = false): Int =
   {
     val selection = Sessions.Selection.session(logic)
     val rc =
       if (!fresh && build(options, selection = selection,
             build_heap = build_heap, no_build = true, dirs = dirs).ok) Process_Result.RC.ok
       else {
         progress.echo("Build started for Isabelle/" + logic + " ...")
         Build.build(options, selection = selection, progress = progress,
           build_heap = build_heap, fresh_build = fresh, dirs = dirs).rc
       }
     if (strict && rc != Process_Result.RC.ok) error("Failed to build Isabelle/" + logic) else rc
   }
 }
diff --git a/src/Pure/Tools/build_job.scala b/src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala
+++ b/src/Pure/Tools/build_job.scala
@@ -1,555 +1,552 @@
 /*  Title:      Pure/Tools/build_job.scala
     Author:     Makarius
 
 Build job running prover process, with rudimentary PIDE session.
 */
 
 package isabelle
 
 
 import java.util.HashMap
 
 import scala.collection.mutable
 
 
 object Build_Job
 {
   /* theory markup/messages from database */
 
   def read_theory(
     db_context: Sessions.Database_Context,
-    resources: Resources,
     session_hierarchy: List[String],
     theory: String,
     unicode_symbols: Boolean = false): Option[Command] =
   {
     def read(name: String): Export.Entry =
       db_context.get_export(session_hierarchy, theory, name)
 
     def read_xml(name: String): XML.Body =
       YXML.parse_body(
         Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed)),
         cache = db_context.cache)
 
     (read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match {
       case (Value.Long(id), thy_file :: blobs_files) =>
-        val node_name = resources.file_node(Path.explode(thy_file), theory = theory)
+        val node_name = Resources.file_node(Path.explode(thy_file), theory = theory)
 
         val results =
           Command.Results.make(
             for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES))
               yield i -> elem)
 
         val blobs =
           blobs_files.map(file =>
           {
             val path = Path.explode(file)
-            val name = resources.file_node(path)
+            val name = Resources.file_node(path)
             val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path)
             Command.Blob(name, src_path, None)
           })
         val blobs_xml =
           for (i <- (1 to blobs.length).toList)
             yield read_xml(Export.MARKUP + i)
 
         val blobs_info =
           Command.Blobs_Info(
             for { (Command.Blob(name, src_path, _), xml) <- blobs zip blobs_xml }
               yield {
                 val text = XML.content(xml)
                 val chunk = Symbol.Text_Chunk(text)
                 val digest = SHA1.digest(Symbol.encode(text))
                 Exn.Res(Command.Blob(name, src_path, Some((digest, chunk))))
               })
 
         val thy_xml = read_xml(Export.MARKUP)
         val thy_source = XML.content(thy_xml)
 
         val markups_index =
           Command.Markup_Index.markup :: blobs.map(Command.Markup_Index.blob)
         val markups =
           Command.Markups.make(
             for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml))
             yield index -> Markup_Tree.from_XML(xml))
 
         val command =
           Command.unparsed(thy_source, theory = true, id = id, node_name = node_name,
             blobs_info = blobs_info, results = results, markups = markups)
         Some(command)
       case _ => None
     }
   }
 
 
   /* print messages */
 
   def print_log(
     options: Options,
     session_name: String,
     theories: List[String] = Nil,
     verbose: Boolean = false,
     progress: Progress = new Progress,
     margin: Double = Pretty.default_margin,
     breakgain: Double = Pretty.default_breakgain,
     metric: Pretty.Metric = Symbol.Metric,
     unicode_symbols: Boolean = false): Unit =
   {
     val store = Sessions.store(options)
-    val resources = Resources.empty
-    val session = new Session(options, resources)
+    val session = new Session(options, Resources.empty)
 
     using(store.open_database_context())(db_context =>
     {
       val result =
         db_context.input_database(session_name)((db, _) =>
         {
           val theories = store.read_theories(db, session_name)
           val errors = store.read_errors(db, session_name)
           store.read_build(db, session_name).map(info => (theories, errors, info.return_code))
         })
       result match {
         case None => error("Missing build database for session " + quote(session_name))
         case Some((used_theories, errors, rc)) =>
           theories.filterNot(used_theories.toSet) match {
             case Nil =>
             case bad => error("Unknown theories " + commas_quote(bad))
           }
           val print_theories =
             if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
           for (thy <- print_theories) {
             val thy_heading = "\nTheory " + quote(thy) + ":"
-            read_theory(db_context, resources, List(session_name), thy,
-              unicode_symbols = unicode_symbols)
+            read_theory(db_context, List(session_name), thy, unicode_symbols = unicode_symbols)
             match {
               case None => progress.echo(thy_heading + " MISSING")
               case Some(command) =>
                 val snapshot = Document.State.init.snippet(command)
                 val rendering = new Rendering(snapshot, options, session)
                 val messages =
                   rendering.text_messages(Text.Range.full)
                     .filter(message => verbose || Protocol.is_exported(message.info))
                 if (messages.nonEmpty) {
                   val line_document = Line.Document(command.source)
                   progress.echo(thy_heading)
                   for (Text.Info(range, elem) <- messages) {
                     val line = line_document.position(range.start).line1
                     val pos = Position.Line_File(line, command.node_name.node)
                     progress.echo(
                       Protocol.message_text(elem, heading = true, pos = pos,
                         margin = margin, breakgain = breakgain, metric = metric))
                   }
                 }
             }
           }
 
           if (errors.nonEmpty) {
             val msg = Symbol.output(unicode_symbols, cat_lines(errors))
             progress.echo("\nBuild errors:\n" + Output.error_message_text(msg))
           }
           if (rc != Process_Result.RC.ok) {
             progress.echo("\n" + Process_Result.RC.print_long(rc))
           }
       }
     })
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool = Isabelle_Tool("log", "print messages from build database",
     Scala_Project.here, args =>
   {
     /* arguments */
 
     var unicode_symbols = false
     var theories: List[String] = Nil
     var margin = Pretty.default_margin
     var options = Options.init()
     var verbose = false
 
     val getopts = Getopts("""
 Usage: isabelle log [OPTIONS] SESSION
 
   Options are:
     -T NAME      restrict to given theories (multiple options possible)
     -U           output Unicode symbols
     -m MARGIN    margin for pretty printing (default: """ + margin + """)
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           print all messages, including information etc.
 
   Print messages from the build database of the given session, without any
   checks against current sources: results from a failed build can be
   printed as well.
 """,
       "T:" -> (arg => theories = theories ::: List(arg)),
       "U" -> (_ => unicode_symbols = true),
       "m:" -> (arg => margin = Value.Double.parse(arg)),
       "o:" -> (arg => options = options + arg),
       "v" -> (_ => verbose = true))
 
     val more_args = getopts(args)
     val session_name =
       more_args match {
         case List(session_name) => session_name
         case _ => getopts.usage()
       }
 
     val progress = new Console_Progress()
 
     print_log(options, session_name, theories = theories, verbose = verbose, margin = margin,
       progress = progress, unicode_symbols = unicode_symbols)
   })
 }
 
 class Build_Job(progress: Progress,
   session_name: String,
   val info: Sessions.Info,
   deps: Sessions.Deps,
   store: Sessions.Store,
   do_store: Boolean,
   log: Logger,
   session_setup: (String, Session) => Unit,
   val numa_node: Option[Int],
   command_timings0: List[Properties.T])
 {
   val options: Options = NUMA.policy_options(info.options, numa_node)
 
   private val sessions_structure = deps.sessions_structure
 
   private val future_result: Future[Process_Result] =
     Future.thread("build", uninterruptible = true) {
       val parent = info.parent.getOrElse("")
       val base = deps(parent)
       val result_base = deps(session_name)
 
       val env = new HashMap(Isabelle_System.settings())
       env.put("ISABELLE_ML_DEBUGGER", options.bool("ML_debugger").toString)
 
       val is_pure = Sessions.is_pure(session_name)
 
       val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil
 
       val eval_store =
         if (do_store) {
           (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) :::
           List("ML_Heap.save_child " +
             ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name))))
         }
         else Nil
 
       val resources =
         new Resources(sessions_structure, base, log = log, command_timings = command_timings0)
       val session =
         new Session(options, resources) {
           override val cache: Term.Cache = store.cache
 
           override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
           {
             result_base.load_commands.get(name.expand) match {
               case Some(spans) =>
                 val syntax = result_base.theory_syntax(name)
                 Command.build_blobs_info(syntax, name, spans)
               case None => Command.Blobs_Info.none
             }
           }
         }
 
       object Build_Session_Errors
       {
         private val promise: Promise[List[String]] = Future.promise
 
         def result: Exn.Result[List[String]] = promise.join_result
         def cancel(): Unit = promise.cancel()
         def apply(errs: List[String]): Unit =
         {
           try { promise.fulfill(errs) }
           catch { case _: IllegalStateException => }
         }
       }
 
       val export_consumer =
         Export.consumer(store.open_database(session_name, output = true), store.cache,
           progress = progress)
 
       val stdout = new StringBuilder(1000)
       val stderr = new StringBuilder(1000)
       val command_timings = new mutable.ListBuffer[Properties.T]
       val theory_timings = new mutable.ListBuffer[Properties.T]
       val session_timings = new mutable.ListBuffer[Properties.T]
       val runtime_statistics = new mutable.ListBuffer[Properties.T]
       val task_statistics = new mutable.ListBuffer[Properties.T]
 
       def fun(
         name: String,
         acc: mutable.ListBuffer[Properties.T],
         unapply: Properties.T => Option[Properties.T]): (String, Session.Protocol_Function) =
       {
         name -> ((msg: Prover.Protocol_Output) =>
           unapply(msg.properties) match {
             case Some(props) => acc += props; true
             case _ => false
           })
       }
 
       session.init_protocol_handler(new Session.Protocol_Handler
         {
           override def exit(): Unit = Build_Session_Errors.cancel()
 
           private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
           {
             val (rc, errors) =
               try {
                 val (rc, errs) =
                 {
                   import XML.Decode._
                   pair(int, list(x => x))(Symbol.decode_yxml(msg.text))
                 }
                 val errors =
                   for (err <- errs) yield {
                     val prt = Protocol_Message.expose_no_reports(err)
                     Pretty.string_of(prt, metric = Symbol.Metric)
                   }
                 (rc, errors)
               }
               catch { case ERROR(err) => (Process_Result.RC.failure, List(err)) }
 
             session.protocol_command("Prover.stop", rc.toString)
             Build_Session_Errors(errors)
             true
           }
 
           private def loading_theory(msg: Prover.Protocol_Output): Boolean =
             msg.properties match {
               case Markup.Loading_Theory(Markup.Name(name)) =>
                 progress.theory(Progress.Theory(name, session = session_name))
                 false
               case _ => false
             }
 
           private def export_(msg: Prover.Protocol_Output): Boolean =
             msg.properties match {
               case Protocol.Export(args) =>
                 export_consumer(session_name, args, msg.chunk)
                 true
               case _ => false
             }
 
           override val functions =
             List(
               Markup.Build_Session_Finished.name -> build_session_finished,
               Markup.Loading_Theory.name -> loading_theory,
               Markup.EXPORT -> export_,
               fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
               fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply),
               fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
         })
 
       session.command_timings += Session.Consumer("command_timings")
         {
           case Session.Command_Timing(props) =>
             for {
               elapsed <- Markup.Elapsed.unapply(props)
               elapsed_time = Time.seconds(elapsed)
               if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold")
             } command_timings += props.filter(Markup.command_timing_property)
         }
 
       session.runtime_statistics += Session.Consumer("ML_statistics")
         {
           case Session.Runtime_Statistics(props) => runtime_statistics += props
         }
 
       session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories")
         {
           case snapshot =>
             if (!progress.stopped) {
               val rendering = new Rendering(snapshot, options, session)
 
               def export_(name: String, xml: XML.Body, compress: Boolean = true): Unit =
               {
                 if (!progress.stopped) {
                   val theory_name = snapshot.node_name.theory
                   val args =
                     Protocol.Export.Args(theory_name = theory_name, name = name, compress = compress)
                   val bytes = Bytes(Symbol.encode(YXML.string_of_body(xml)))
                   if (!bytes.is_empty) export_consumer(session_name, args, bytes)
                 }
               }
               def export_text(name: String, text: String, compress: Boolean = true): Unit =
                 export_(name, List(XML.Text(text)), compress = compress)
 
               for (command <- snapshot.snippet_command) {
                 export_text(Export.DOCUMENT_ID, command.id.toString, compress = false)
               }
 
               export_text(Export.FILES,
                 cat_lines(snapshot.node_files.map(_.symbolic.node)), compress = false)
 
               for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) {
                 export_(Export.MARKUP + (i + 1), xml)
               }
               export_(Export.MARKUP, snapshot.xml_markup())
               export_(Export.MESSAGES, snapshot.messages.map(_._1))
 
               val citations = Library.distinct(rendering.citations(Text.Range.full).map(_.info))
               export_text(Export.DOCUMENT_CITATIONS, cat_lines(citations))
             }
         }
 
       session.all_messages += Session.Consumer[Any]("build_session_output")
         {
           case msg: Prover.Output =>
             val message = msg.message
             if (msg.is_system) resources.log(Protocol.message_text(message))
 
             if (msg.is_stdout) {
               stdout ++= Symbol.encode(XML.content(message))
             }
             else if (msg.is_stderr) {
               stderr ++= Symbol.encode(XML.content(message))
             }
             else if (msg.is_exit) {
               val err =
                 "Prover terminated" +
                   (msg.properties match {
                     case Markup.Process_Result(result) => ": " + result.print_rc
                     case _ => ""
                   })
               Build_Session_Errors(List(err))
             }
           case _ =>
         }
 
       session_setup(session_name, session)
 
       val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
 
       val process =
         Isabelle_Process.start(session, options, sessions_structure, store,
           logic = parent, raw_ml_system = is_pure,
           use_prelude = use_prelude, eval_main = eval_main,
           cwd = info.dir.file, env = env)
 
       val build_errors =
         Isabelle_Thread.interrupt_handler(_ => process.terminate()) {
           Exn.capture { process.await_startup() } match {
             case Exn.Res(_) =>
               val resources_yxml = resources.init_session_yxml
               val encode_options: XML.Encode.T[Options] =
                 options => session.prover_options(options).encode
               val args_yxml =
                 YXML.string_of_body(
                   {
                     import XML.Encode._
                     pair(string, list(pair(encode_options, list(pair(string, properties)))))(
                       (session_name, info.theories))
                   })
               session.protocol_command("build_session", resources_yxml, args_yxml)
               Build_Session_Errors.result
             case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn)))
           }
         }
 
       val process_result =
         Isabelle_Thread.interrupt_handler(_ => process.terminate()) { process.await_shutdown() }
 
       session.stop()
 
       val export_errors =
         export_consumer.shutdown(close = true).map(Output.error_message_text)
 
       val (document_output, document_errors) =
         try {
           if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) {
             using(store.open_database_context())(db_context =>
               {
                 val documents =
                   Document_Build.build_documents(
                     Document_Build.context(session_name, deps, db_context, progress = progress),
                     output_sources = info.document_output,
                     output_pdf = info.document_output)
                 db_context.output_database(session_name)(db =>
                   documents.foreach(_.write(db, session_name)))
                 (documents.flatMap(_.log_lines), Nil)
               })
           }
           else (Nil, Nil)
         }
         catch {
           case exn: Document_Build.Build_Error => (exn.log_lines, List(exn.message))
           case Exn.Interrupt.ERROR(msg) => (Nil, List(msg))
         }
 
       val result =
       {
         val theory_timing =
           theory_timings.iterator.map(
             { case props @ Markup.Name(name) => name -> props }).toMap
         val used_theory_timings =
           for { (name, _) <- deps(session_name).used_theories }
             yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory))
 
         val more_output =
           Library.trim_line(stdout.toString) ::
             command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
             used_theory_timings.map(Protocol.Theory_Timing_Marker.apply) :::
             session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
             runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
             task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::
             document_output
 
         process_result.output(more_output)
           .error(Library.trim_line(stderr.toString))
           .errors_rc(export_errors ::: document_errors)
       }
 
       build_errors match {
         case Exn.Res(build_errs) =>
           val errs = build_errs ::: document_errors
           if (errs.nonEmpty) {
             result.error_rc.output(
               errs.flatMap(s => split_lines(Output.error_message_text(s))) :::
                 errs.map(Protocol.Error_Message_Marker.apply))
           }
           else if (progress.stopped && result.ok) result.copy(rc = Process_Result.RC.interrupt)
           else result
         case Exn.Exn(Exn.Interrupt()) =>
           if (result.ok) result.copy(rc = Process_Result.RC.interrupt)
           else result
         case Exn.Exn(exn) => throw exn
       }
     }
 
   def terminate(): Unit = future_result.cancel()
   def is_finished: Boolean = future_result.is_finished
 
   private val timeout_request: Option[Event_Timer.Request] =
   {
     if (info.timeout_ignored) None
     else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() })
   }
 
   def join: (Process_Result, Option[String]) =
   {
     val result1 = future_result.join
 
     val was_timeout =
       timeout_request match {
         case None => false
         case Some(request) => !request.cancel()
       }
 
     val result2 =
       if (result1.ok) result1
       else if (was_timeout) result1.error(Output.error_message_text("Timeout")).timeout_rc
       else if (result1.interrupted) result1.error(Output.error_message_text("Interrupt"))
       else result1
 
     val heap_digest =
       if (result2.ok && do_store && store.output_heap(session_name).is_file)
         Some(Sessions.write_heap_digest(store.output_heap(session_name)))
       else None
 
     (result2, heap_digest)
   }
 }
diff --git a/src/Pure/Tools/profiling_report.scala b/src/Pure/Tools/profiling_report.scala
--- a/src/Pure/Tools/profiling_report.scala
+++ b/src/Pure/Tools/profiling_report.scala
@@ -1,86 +1,85 @@
 /*  Title:      Pure/Tools/profiling_report.scala
     Author:     Makarius
 
 Report Poly/ML profiling information from session build database.
 */
 
 package isabelle
 
 
 object Profiling_Report
 {
   def profiling_report(
     options: Options,
     session: String,
     theories: List[String] = Nil,
     clean_name: Boolean = false,
     progress: Progress = new Progress): Unit =
   {
     val store = Sessions.store(options)
-    val resources = Resources.empty
 
     using(store.open_database_context())(db_context =>
     {
       val result =
         db_context.input_database(session)((db, name) => Some(store.read_theories(db, name)))
       result match {
         case None => error("Missing build database for session " + quote(session))
         case Some(used_theories) =>
           theories.filterNot(used_theories.toSet) match {
             case Nil =>
             case bad => error("Unknown theories " + commas_quote(bad))
           }
           val reports =
             (for {
               thy <- used_theories.iterator
               if theories.isEmpty || theories.contains(thy)
-              command <- Build_Job.read_theory(db_context, resources, List(session), thy).iterator
+              command <- Build_Job.read_theory(db_context, List(session), thy).iterator
               snapshot = Document.State.init.snippet(command)
               (Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator
             } yield if (clean_name) report.clean_name else report).toList
 
           for (report <- ML_Profiling.account(reports)) progress.echo(report.print)
       }
     })
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files",
       Scala_Project.here, args =>
     {
       var theories: List[String] = Nil
       var clean_name = false
       var options = Options.init()
 
       val getopts =
         Getopts("""
 Usage: isabelle profiling_report [OPTIONS] SESSION
 
   Options are:
     -T NAME      restrict to given theories (multiple options possible)
     -c           clean function names
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
 
   Report Poly/ML profiling from the build database of the given session
   (without up-to-date check of sources).
 """,
           "T:" -> (arg => theories = theories ::: List(arg)),
           "c" -> (_ => clean_name = true),
           "o:" -> (arg => options = options + arg))
 
       val more_args = getopts(args)
       val session_name =
         more_args match {
           case List(session_name) => session_name
           case _ => getopts.usage()
         }
 
       val progress = new Console_Progress()
 
       profiling_report(options, session_name, theories = theories,
         clean_name = clean_name, progress = progress)
     })
 }
diff --git a/src/Tools/VSCode/src/preview_panel.scala b/src/Tools/VSCode/src/preview_panel.scala
--- a/src/Tools/VSCode/src/preview_panel.scala
+++ b/src/Tools/VSCode/src/preview_panel.scala
@@ -1,47 +1,46 @@
 /*  Title:      Tools/VSCode/src/preview_panel.scala
     Author:     Makarius
 
 HTML document preview.
 */
 
 package isabelle.vscode
 
 
 import isabelle._
 
 import java.io.{File => JFile}
 
 
 class Preview_Panel(resources: VSCode_Resources)
 {
   private val pending = Synchronized(Map.empty[JFile, Int])
 
   def request(file: JFile, column: Int): Unit =
     pending.change(map => map + (file -> column))
 
   def flush(channel: Channel): Boolean =
   {
     pending.change_result(map =>
     {
       val map1 =
         map.iterator.foldLeft(map) {
           case (m, (file, column)) =>
             resources.get_model(file) match {
               case Some(model) =>
                 val snapshot = model.snapshot()
                 if (snapshot.is_outdated) m
                 else {
                   val html_context = Presentation.html_context()
                   val document =
-                    Presentation.html_document(
-                      resources, snapshot, html_context, Presentation.elements2)
+                    Presentation.html_document(snapshot, html_context, Presentation.elements2)
                   channel.write(LSP.Preview_Response(file, column, document.title, document.content))
                   m - file
                 }
               case None => m - file
             }
         }
       (map1.nonEmpty, map1)
     })
   }
 }
diff --git a/src/Tools/jEdit/src/document_model.scala b/src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala
+++ b/src/Tools/jEdit/src/document_model.scala
@@ -1,703 +1,703 @@
 /*  Title:      Tools/jEdit/src/document_model.scala
     Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
 Document model connected to jEdit buffer or external file: content of theory
 node or auxiliary file (blob).
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import java.io.{File => JFile}
 
 import scala.collection.mutable
 import scala.annotation.tailrec
 
 import org.gjt.sp.jedit.View
 import org.gjt.sp.jedit.Buffer
 import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
 
 
 object Document_Model
 {
   /* document models */
 
   sealed case class State(
     models: Map[Document.Node.Name, Document_Model] = Map.empty,
     buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty,
     overlays: Document.Overlays = Document.Overlays.empty)
   {
     def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] =
       for {
         (node_name, model) <- models.iterator
         if model.isInstanceOf[File_Model]
       } yield (node_name, model.asInstanceOf[File_Model])
 
     def document_blobs: Document.Blobs =
       Document.Blobs(
         (for {
           (node_name, model) <- models.iterator
           blob <- model.get_blob
         } yield (node_name -> blob)).toMap)
 
     def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer)
       : (Buffer_Model, State) =
     {
       val old_model =
         models.get(node_name) match {
           case Some(file_model: File_Model) => Some(file_model)
           case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit())
           case _ => None
         }
       val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model)
       (buffer_model,
         copy(models = models + (node_name -> buffer_model),
           buffer_models = buffer_models + (buffer -> buffer_model)))
     }
 
     def close_buffer(buffer: JEditBuffer): State =
     {
       buffer_models.get(buffer) match {
         case None => this
         case Some(buffer_model) =>
           val file_model = buffer_model.exit()
           copy(models = models + (file_model.node_name -> file_model),
             buffer_models = buffer_models - buffer)
       }
     }
 
     def provide_file(session: Session, node_name: Document.Node.Name, text: String): State =
       if (models.isDefinedAt(node_name)) this
       else {
         val edit = Text.Edit.insert(0, text)
         val model = File_Model.init(session, node_name, text, pending_edits = List(edit))
         copy(models = models + (node_name -> model))
       }
   }
 
   private val state = Synchronized(State())  // owned by GUI thread
 
   def reset(): Unit = state.change(_ => State())
 
   def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
   def get(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
   def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
 
   def document_blobs(): Document.Blobs = state.value.document_blobs
 
 
   /* bibtex */
 
   def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
     Bibtex.entries_iterator(state.value.models)
 
   def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
       : Option[Completion.Result] =
     Bibtex.completion(history, rendering, caret, state.value.models)
 
 
   /* overlays */
 
   def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
     state.value.overlays(name)
 
   def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
     state.change(st => st.copy(overlays = st.overlays.insert(command, fn, args)))
 
   def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
     state.change(st => st.copy(overlays = st.overlays.remove(command, fn, args)))
 
 
   /* sync external files */
 
   def sync_files(changed_files: Set[JFile]): Boolean =
   {
     state.change_result(st =>
       {
         val changed_models =
           (for {
             (node_name, model) <- st.file_models_iterator
             file <- model.file if changed_files(file)
             text <- PIDE.resources.read_file_content(node_name)
             if model.content.text != text
           } yield {
             val content = Document_Model.File_Content(text)
             val edits = Text.Edit.replace(0, model.content.text, text)
             (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits))
           }).toList
         if (changed_models.isEmpty) (false, st)
         else (true, st.copy(models = changed_models.foldLeft(st.models)(_ + _)))
       })
   }
 
 
   /* syntax */
 
   def syntax_changed(names: List[Document.Node.Name]): Unit =
   {
     GUI_Thread.require {}
 
     val models = state.value.models
     for (name <- names.iterator; model <- models.get(name)) {
       model match { case buffer_model: Buffer_Model => buffer_model.syntax_changed() case _ => }
     }
   }
 
 
   /* init and exit */
 
   def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model =
   {
     GUI_Thread.require {}
     state.change_result(st =>
       st.buffer_models.get(buffer) match {
         case Some(buffer_model) if buffer_model.node_name == node_name =>
           buffer_model.init_token_marker()
           (buffer_model, st)
         case _ =>
           val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer)
           buffer.propertiesChanged()
           res
       })
   }
 
   def exit(buffer: Buffer): Unit =
   {
     GUI_Thread.require {}
     state.change(st =>
       if (st.buffer_models.isDefinedAt(buffer)) {
         val res = st.close_buffer(buffer)
         buffer.propertiesChanged()
         res
       }
       else st)
   }
 
   def provide_files(session: Session, files: List[(Document.Node.Name, String)]): Unit =
   {
     GUI_Thread.require {}
     state.change(st =>
       files.foldLeft(st) {
         case (st1, (node_name, text)) => st1.provide_file(session, node_name, text)
       })
   }
 
 
   /* required nodes */
 
   def required_nodes(): Set[Document.Node.Name] =
     (for {
       (node_name, model) <- state.value.models.iterator
       if model.node_required
     } yield node_name).toSet
 
   def node_required(
     name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false): Unit =
   {
     GUI_Thread.require {}
 
     val changed =
       state.change_result(st =>
         st.models.get(name) match {
           case None => (false, st)
           case Some(model) =>
             val required = if (toggle) !model.node_required else set
             model match {
               case model1: File_Model if required != model1.node_required =>
                 (true, st.copy(models = st.models + (name -> model1.copy(node_required = required))))
               case model1: Buffer_Model if required != model1.node_required =>
                 model1.set_node_required(required); (true, st)
               case _ => (false, st)
             }
         })
     if (changed) {
       PIDE.plugin.options_changed()
       PIDE.editor.flush()
     }
   }
 
   def view_node_required(view: View, toggle: Boolean = false, set: Boolean = false): Unit =
     Document_Model.get(view.getBuffer).foreach(model =>
       node_required(model.node_name, toggle = toggle, set = set))
 
 
   /* flushed edits */
 
   def flush_edits(hidden: Boolean, purge: Boolean): (Document.Blobs, List[Document.Edit_Text]) =
   {
     GUI_Thread.require {}
 
     state.change_result(st =>
       {
         val doc_blobs = st.document_blobs
 
         val buffer_edits =
           (for {
             (_, model) <- st.buffer_models.iterator
             edit <- model.flush_edits(doc_blobs, hidden).iterator
           } yield edit).toList
 
         val file_edits =
           (for {
             (node_name, model) <- st.file_models_iterator
             (edits, model1) <- model.flush_edits(doc_blobs, hidden)
           } yield (edits, node_name -> model1)).toList
 
         val model_edits = buffer_edits ::: file_edits.flatMap(_._1)
 
         val purge_edits =
           if (purge) {
             val purged =
               (for ((node_name, model) <- st.file_models_iterator)
                yield (node_name -> model.purge_edits(doc_blobs))).toList
 
             val imports =
             {
               val open_nodes =
                 (for ((_, model) <- st.buffer_models.iterator) yield model.node_name).toList
               val touched_nodes = model_edits.map(_._1)
               val pending_nodes = for ((node_name, None) <- purged) yield node_name
               (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
             }
             val retain = PIDE.resources.dependencies(imports).theories.toSet
 
             for ((node_name, Some(edits)) <- purged if !retain(node_name); edit <- edits)
               yield edit
           }
           else Nil
 
         val st1 = st.copy(models = st.models ++ file_edits.map(_._2) -- purge_edits.map(_._1))
         PIDE.plugin.file_watcher.purge(
           (for {
             (_, model) <- st1.file_models_iterator
             file <- model.file
           } yield file.getParentFile).toSet)
 
         ((doc_blobs, model_edits ::: purge_edits), st1)
       })
   }
 
 
   /* file content */
 
   sealed case class File_Content(text: String)
   {
     lazy val bytes: Bytes = Bytes(Symbol.encode(text))
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
     lazy val bibtex_entries: List[Text.Info[String]] =
       try { Bibtex.entries(text) }
       catch { case ERROR(_) => Nil }
   }
 
 
   /* HTTP preview */
 
   private val plain_text_prefix = "plain_text="
 
   def open_preview(view: View, plain_text: Boolean): Unit =
   {
     Document_Model.get(view.getBuffer) match {
       case Some(model) =>
         val name = model.node_name
         val url =
           PIDE.plugin.http_server.url + PIDE.plugin.http_root + "/preview?" +
             (if (plain_text) plain_text_prefix else "") + Url.encode(name.node)
         PIDE.editor.hyperlink_url(url).follow(view)
       case _ =>
     }
   }
 
   def http_handlers(http_root: String): List[HTTP.Handler] =
   {
     val fonts_root = http_root + "/fonts"
     val preview_root = http_root + "/preview"
 
     val html =
       HTTP.Handler.get(preview_root, arg =>
         for {
           query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode)
           name = Library.perhaps_unprefix(plain_text_prefix, query)
           model <- get(PIDE.resources.node_name(name))
         }
         yield {
           val snapshot = model.await_stable_snapshot()
           val html_context = Presentation.html_context()
           val document =
             Presentation.html_document(
-              PIDE.resources, snapshot, html_context, Presentation.elements2,
+              snapshot, html_context, Presentation.elements2,
               plain_text = query.startsWith(plain_text_prefix),
               fonts_css = HTML.fonts_css_dir(http_root))
           HTTP.Response.html(document.content)
         })
 
     List(HTTP.welcome(http_root), HTTP.fonts(fonts_root), html)
   }
 }
 
 sealed abstract class Document_Model extends Document.Model
 {
   /* perspective */
 
   def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil
 
   def node_perspective(
     doc_blobs: Document.Blobs, hidden: Boolean): (Boolean, Document.Node.Perspective_Text) =
   {
     GUI_Thread.require {}
 
     if (Isabelle.continuous_checking && is_theory) {
       val snapshot = this.snapshot()
 
       val reparse = snapshot.node.load_commands_changed(doc_blobs)
       val perspective =
         if (hidden) Text.Perspective.empty
         else {
           val view_ranges = document_view_ranges(snapshot)
           val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node)
           Text.Perspective(view_ranges ::: load_ranges)
         }
       val overlays = PIDE.editor.node_overlays(node_name)
 
       (reparse, Document.Node.Perspective(node_required, perspective, overlays))
     }
     else (false, Document.Node.no_perspective_text)
   }
 
 
   /* snapshot */
 
   @tailrec final def await_stable_snapshot(): Document.Snapshot =
   {
     val snapshot = this.snapshot()
     if (snapshot.is_outdated) {
       PIDE.options.seconds("editor_output_delay").sleep()
       await_stable_snapshot()
     }
     else snapshot
   }
 }
 
 object File_Model
 {
   def empty(session: Session): File_Model =
     File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
       false, Document.Node.no_perspective_text, Nil)
 
   def init(session: Session,
     node_name: Document.Node.Name,
     text: String,
     node_required: Boolean = false,
     last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
     pending_edits: List[Text.Edit] = Nil): File_Model =
   {
     val file = JEdit_Lib.check_file(node_name.node)
     file.foreach(PIDE.plugin.file_watcher.register_parent(_))
 
     val content = Document_Model.File_Content(text)
     val node_required1 = node_required || File_Format.registry.is_theory(node_name)
     File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits)
   }
 }
 
 case class File_Model(
   session: Session,
   node_name: Document.Node.Name,
   file: Option[JFile],
   content: Document_Model.File_Content,
   node_required: Boolean,
   last_perspective: Document.Node.Perspective_Text,
   pending_edits: List[Text.Edit]) extends Document_Model
 {
   /* text */
 
   def get_text(range: Text.Range): Option[String] =
     range.try_substring(content.text)
 
 
   /* header */
 
   def node_header: Document.Node.Header =
     PIDE.resources.special_header(node_name) getOrElse
       PIDE.resources.check_thy(node_name, Scan.char_reader(content.text), strict = false)
 
 
   /* content */
 
   def node_position(offset: Text.Offset): Line.Node_Position =
     Line.Node_Position(node_name.node,
       Line.Position.zero.advance(content.text.substring(0, offset)))
 
   def get_blob: Option[Document.Blob] =
     if (is_theory) None
     else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
 
   def bibtex_entries: List[Text.Info[String]] =
     if (Bibtex.is_bibtex(node_name.node)) content.bibtex_entries else Nil
 
 
   /* edits */
 
   def update_text(text: String): Option[File_Model] =
     Text.Edit.replace(0, content.text, text) match {
       case Nil => None
       case edits =>
         val content1 = Document_Model.File_Content(text)
         val pending_edits1 = pending_edits ::: edits
         Some(copy(content = content1, pending_edits = pending_edits1))
     }
 
   def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean)
     : Option[(List[Document.Edit_Text], File_Model)] =
   {
     val (reparse, perspective) = node_perspective(doc_blobs, hidden)
     if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
       val edits = node_edits(node_header, pending_edits, perspective)
       Some((edits, copy(last_perspective = perspective, pending_edits = Nil)))
     }
     else None
   }
 
   def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] =
     if (pending_edits.nonEmpty ||
         !File_Format.registry.is_theory(node_name) &&
           (node_required || !Document.Node.is_no_perspective_text(last_perspective))) None
     else {
       val text_edits = List(Text.Edit.remove(0, content.text))
       Some(node_edits(Document.Node.no_header, text_edits, Document.Node.no_perspective_text))
     }
 
 
   /* snapshot */
 
   def is_stable: Boolean = pending_edits.isEmpty
   def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
 }
 
 case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
   extends Document_Model
 {
   /* text */
 
   def get_text(range: Text.Range): Option[String] =
     JEdit_Lib.get_text(buffer, range)
 
 
   /* header */
 
   def node_header(): Document.Node.Header =
   {
     GUI_Thread.require {}
 
     PIDE.resources.special_header(node_name) getOrElse
       JEdit_Lib.buffer_lock(buffer) {
         PIDE.resources.check_thy(node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
       }
   }
 
 
   /* perspective */
 
   // owned by GUI thread
   private var _node_required = false
   def node_required: Boolean = _node_required
   def set_node_required(b: Boolean): Unit = GUI_Thread.require { _node_required = b }
 
   def document_view_iterator: Iterator[Document_View] =
     for {
       text_area <- JEdit_Lib.jedit_text_areas(buffer)
       doc_view <- Document_View.get(text_area)
     } yield doc_view
 
   override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] =
   {
     GUI_Thread.require {}
 
     (for {
       doc_view <- document_view_iterator
       range <- doc_view.perspective(snapshot).ranges.iterator
     } yield range).toList
   }
 
 
   /* blob */
 
   // owned by GUI thread
   private var _blob: Option[(Bytes, String, Symbol.Text_Chunk)] = None
 
   private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
 
   def get_blob: Option[Document.Blob] =
     GUI_Thread.require {
       if (is_theory) None
       else {
         val (bytes, text, chunk) =
           _blob match {
             case Some(x) => x
             case None =>
               val bytes = PIDE.resources.make_file_content(buffer)
               val text = buffer.getText(0, buffer.getLength)
               val chunk = Symbol.Text_Chunk(text)
               val x = (bytes, text, chunk)
               _blob = Some(x)
               x
           }
         val changed = pending_edits.nonEmpty
         Some(Document.Blob(bytes, text, chunk, changed))
       }
     }
 
 
   /* bibtex entries */
 
   // owned by GUI thread
   private var _bibtex_entries: Option[List[Text.Info[String]]] = None
 
   private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None }
 
   def bibtex_entries: List[Text.Info[String]] =
     GUI_Thread.require {
       if (Bibtex.is_bibtex(node_name.node)) {
         _bibtex_entries match {
           case Some(entries) => entries
           case None =>
             val text = JEdit_Lib.buffer_text(buffer)
             val entries =
               try { Bibtex.entries(text) }
               catch { case ERROR(msg) => Output.warning(msg); Nil }
             _bibtex_entries = Some(entries)
             entries
         }
       }
       else Nil
     }
 
 
   /* pending edits */
 
   private object pending_edits
   {
     private val pending = new mutable.ListBuffer[Text.Edit]
     private var last_perspective = Document.Node.no_perspective_text
 
     def nonEmpty: Boolean = synchronized { pending.nonEmpty }
     def get_edits: List[Text.Edit] = synchronized { pending.toList }
     def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective }
     def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit =
       synchronized { last_perspective = perspective }
 
     def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
       synchronized {
         GUI_Thread.require {}
 
         val edits = get_edits
         val (reparse, perspective) = node_perspective(doc_blobs, hidden)
         if (reparse || edits.nonEmpty || last_perspective != perspective) {
           pending.clear()
           last_perspective = perspective
           node_edits(node_header(), edits, perspective)
         }
         else Nil
       }
 
     def edit(edits: List[Text.Edit]): Unit = synchronized
     {
       GUI_Thread.require {}
 
       reset_blob()
       reset_bibtex_entries()
 
       for (doc_view <- document_view_iterator)
         doc_view.rich_text_area.active_reset()
 
       pending ++= edits
       PIDE.editor.invoke()
     }
   }
 
   def is_stable: Boolean = !pending_edits.nonEmpty
   def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits)
 
   def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
     pending_edits.flush_edits(doc_blobs, hidden)
 
 
   /* buffer listener */
 
   private val buffer_listener: BufferListener = new BufferAdapter
   {
     override def contentInserted(buffer: JEditBuffer,
       start_line: Int, offset: Int, num_lines: Int, length: Int): Unit =
     {
       pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
     }
 
     override def preContentRemoved(buffer: JEditBuffer,
       start_line: Int, offset: Int, num_lines: Int, removed_length: Int): Unit =
     {
       pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
     }
   }
 
 
   /* syntax */
 
   def syntax_changed(): Unit =
   {
     JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0)
     for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
       Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
         invoke(text_area)
     buffer.invalidateCachedFoldLevels()
   }
 
   def init_token_marker(): Unit =
   {
     Isabelle.buffer_token_marker(buffer) match {
       case Some(marker) if marker != buffer.getTokenMarker =>
         buffer.setTokenMarker(marker)
         syntax_changed()
       case _ =>
     }
   }
 
 
   /* init */
 
   def init(old_model: Option[File_Model]): Buffer_Model =
   {
     GUI_Thread.require {}
 
     old_model match {
       case None =>
         pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
       case Some(file_model) =>
         set_node_required(file_model.node_required)
         pending_edits.set_last_perspective(file_model.last_perspective)
         pending_edits.edit(
           file_model.pending_edits :::
             Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer)))
     }
 
     buffer.addBufferListener(buffer_listener)
     init_token_marker()
 
     this
   }
 
 
   /* exit */
 
   def exit(): File_Model =
   {
     GUI_Thread.require {}
 
     buffer.removeBufferListener(buffer_listener)
     init_token_marker()
 
     File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer), node_required,
       pending_edits.get_last_perspective, pending_edits.get_edits)
   }
 }