# HG changeset patch
# User boehmes
# Date 1421354723 -3600
# Node ID e6acec6a6f6f468ff64d89fd5122cad6f719d3cf
# Parent  2f5447b764f9998ac2e1c8dfbbd7894603714208# Parent  6162878e3e539e10bfde061de82cf8dc0943179f
merged

diff -r 2f5447b764f9 -r e6acec6a6f6f Admin/components/components.sha1
--- a/Admin/components/components.sha1	Thu Jan 15 21:44:51 2015 +0100
+++ b/Admin/components/components.sha1	Thu Jan 15 21:45:23 2015 +0100
@@ -93,6 +93,7 @@
 14f20de82b25215a5e055631fb147356400625e6  scala-2.11.1.tar.gz
 4fe9590d08e55760b86755d3fab750e90ac6c380  scala-2.11.2.tar.gz
 27a296495b2167148de06314ed9a942f2dbe23fe  scala-2.11.4.tar.gz
+4b24326541161ce65424293ca9da3e7c2c6ab452  scala-2.11.5.tar.gz
 b447017e81600cc5e30dd61b5d4962f6da01aa80  scala-2.8.1.final.tar.gz
 5659440f6b86db29f0c9c0de7249b7e24a647126  scala-2.9.2.tar.gz
 43b5afbcad575ab6817d2289756ca22fd2ef43a9  spass-3.8ds.tar.gz
diff -r 2f5447b764f9 -r e6acec6a6f6f Admin/components/main
--- a/Admin/components/main	Thu Jan 15 21:44:51 2015 +0100
+++ b/Admin/components/main	Thu Jan 15 21:45:23 2015 +0100
@@ -10,7 +10,7 @@
 jortho-1.0-2
 kodkodi-1.5.2
 polyml-5.5.2-1
-scala-2.11.4
+scala-2.11.5
 spass-3.8ds
 z3-4.3.2pre-1
 xz-java-1.2-1
diff -r 2f5447b764f9 -r e6acec6a6f6f src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Thu Jan 15 21:45:23 2015 +0100
@@ -202,21 +202,28 @@
   qed auto
 qed (auto simp: eq intro: generate_topology.Basis)
 
-lemma borel_measurable_continuous_on_if:
-  assumes A: "A \<in> sets borel" and f: "continuous_on A f" and g: "continuous_on (- A) g"
-  shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> borel_measurable borel"
+lemma borel_measurable_continuous_on_restrict:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+  assumes f: "continuous_on A f"
+  shows "f \<in> borel_measurable (restrict_space borel A)"
 proof (rule borel_measurableI)
   fix S :: "'b set" assume "open S"
-  have "(\<lambda>x. if x \<in> A then f x else g x) -` S \<inter> space borel = (f -` S \<inter> A) \<union> (g -` S \<inter> -A)"
-    by (auto split: split_if_asm)
-  moreover obtain A' where "f -` S \<inter> A = A' \<inter> A" "open A'"
-    using continuous_on_open_invariant[THEN iffD1, rule_format, OF f `open S`] by metis
-  moreover obtain B' where "g -` S \<inter> -A = B' \<inter> -A" "open B'"
-    using continuous_on_open_invariant[THEN iffD1, rule_format, OF g `open S`] by metis
-  ultimately show "(\<lambda>x. if x \<in> A then f x else g x) -` S \<inter> space borel \<in> sets borel"
-    using A by auto
+  with f obtain T where "f -` S \<inter> A = T \<inter> A" "open T"
+    by (metis continuous_on_open_invariant)
+  then show "f -` S \<inter> space (restrict_space borel A) \<in> sets (restrict_space borel A)"
+    by (force simp add: sets_restrict_space space_restrict_space)
 qed
 
+lemma borel_measurable_continuous_on1: "continuous_on UNIV f \<Longrightarrow> f \<in> borel_measurable borel"
+  by (drule borel_measurable_continuous_on_restrict) simp
+
+lemma borel_measurable_continuous_on_if:
+  assumes [measurable]: "A \<in> sets borel" and f: "continuous_on A f" and g: "continuous_on (- A) g"
+  shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> borel_measurable borel"
+  by (rule measurable_piecewise_restrict[where
+       X="\<lambda>b. if b then A else - A" and I=UNIV and f="\<lambda>b x. if b then f x else g x"])
+     (auto intro: f g borel_measurable_continuous_on_restrict)
+
 lemma borel_measurable_continuous_countable_exceptions:
   fixes f :: "'a::t1_space \<Rightarrow> 'b::topological_space"
   assumes X: "countable X"
@@ -229,11 +236,6 @@
     by (intro borel_measurable_continuous_on_if assms continuous_intros)
 qed auto
 
-lemma borel_measurable_continuous_on1:
-  "continuous_on UNIV f \<Longrightarrow> f \<in> borel_measurable borel"
-  using borel_measurable_continuous_on_if[of UNIV f "\<lambda>_. undefined"]
-  by (auto intro: continuous_on_const)
-
 lemma borel_measurable_continuous_on:
   assumes f: "continuous_on UNIV f" and g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. f (g x)) \<in> borel_measurable M"
@@ -636,7 +638,7 @@
     fix x :: 'a assume "a < x \<bullet> i"
     with reals_Archimedean[of "x \<bullet> i - a"]
     obtain n where "a + 1 / real (Suc n) < x \<bullet> i"
-      by (auto simp: inverse_eq_divide field_simps)
+      by (auto simp: field_simps)
     then show "\<exists>n. a + 1 / real (Suc n) \<le> x \<bullet> i"
       by (blast intro: less_imp_le)
   next
@@ -673,7 +675,7 @@
     fix x::'a assume *: "x\<bullet>i < a"
     with reals_Archimedean[of "a - x\<bullet>i"]
     obtain n where "x \<bullet> i < a - 1 / (real (Suc n))"
-      by (auto simp: field_simps inverse_eq_divide)
+      by (auto simp: field_simps)
     then show "\<exists>n. x \<bullet> i \<le> a - 1 / (real (Suc n))"
       by (blast intro: less_imp_le)
   next
@@ -683,7 +685,7 @@
     finally show "x\<bullet>i < a" .
   qed
   show "{x. x\<bullet>i < a} \<in> ?SIGMA" unfolding *
-    by (safe intro!: sets.countable_UN) (auto intro: i)
+    by (intro sets.countable_UN) (auto intro: i)
 qed auto
 
 lemma borel_eq_halfspace_ge:
@@ -693,7 +695,7 @@
   fix a :: real and i :: 'a assume i: "(a, i) \<in> UNIV \<times> Basis"
   have *: "{x::'a. x\<bullet>i < a} = space ?SIGMA - {x::'a. a \<le> x\<bullet>i}" by auto
   show "{x. x\<bullet>i < a} \<in> ?SIGMA" unfolding *
-    using i by (safe intro!: sets.compl_sets) auto
+    using i by (intro sets.compl_sets) auto
 qed auto
 
 lemma borel_eq_halfspace_greater:
@@ -704,7 +706,7 @@
   then have i: "i \<in> Basis" by auto
   have *: "{x::'a. x\<bullet>i \<le> a} = space ?SIGMA - {x::'a. a < x\<bullet>i}" by auto
   show "{x. x\<bullet>i \<le> a} \<in> ?SIGMA" unfolding *
-    by (safe intro!: sets.compl_sets) (auto intro: i)
+    by (intro sets.compl_sets) (auto intro: i)
 qed auto
 
 lemma borel_eq_atMost:
@@ -723,7 +725,7 @@
       by (auto intro!: exI[of _ k])
   qed
   show "{x. x\<bullet>i \<le> a} \<in> ?SIGMA" unfolding *
-    by (safe intro!: sets.countable_UN) auto
+    by (intro sets.countable_UN) auto
 qed auto
 
 lemma borel_eq_greaterThan:
@@ -748,7 +750,7 @@
   qed
   finally show "{x. x\<bullet>i \<le> a} \<in> ?SIGMA"
     apply (simp only:)
-    apply (safe intro!: sets.countable_UN sets.Diff)
+    apply (intro sets.countable_UN sets.Diff)
     apply (auto intro: sigma_sets_top)
     done
 qed auto
@@ -774,7 +776,7 @@
   qed
   finally show "{x. a \<le> x\<bullet>i} \<in> ?SIGMA"
     apply (simp only:)
-    apply (safe intro!: sets.countable_UN sets.Diff)
+    apply (intro sets.countable_UN sets.Diff)
     apply (auto intro: sigma_sets_top )
     done
 qed auto
@@ -797,7 +799,7 @@
       by (auto intro!: exI[of _ k])
   qed
   show "{..a} \<in> ?SIGMA" unfolding *
-    by (safe intro!: sets.countable_UN)
+    by (intro sets.countable_UN)
        (auto intro!: sigma_sets_top)
 qed auto
 
@@ -822,7 +824,7 @@
   have "{..<x} = (\<Union>i::nat. {-real i ..< x})"
     by (auto simp: move_uminus real_arch_simple)
   then show "{y. y <e x} \<in> ?SIGMA"
-    by (auto intro: sigma_sets.intros simp: eucl_lessThan)
+    by (auto intro: sigma_sets.intros(2-) simp: eucl_lessThan)
 qed auto
 
 lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)"
@@ -831,15 +833,13 @@
   fix x :: "'a set" assume "open x"
   hence "x = UNIV - (UNIV - x)" by auto
   also have "\<dots> \<in> sigma_sets UNIV (Collect closed)"
-    by (rule sigma_sets.Compl)
-       (auto intro!: sigma_sets.Basic simp: `open x`)
+    by (force intro: sigma_sets.Compl simp: `open x`)
   finally show "x \<in> sigma_sets UNIV (Collect closed)" by simp
 next
   fix x :: "'a set" assume "closed x"
   hence "x = UNIV - (UNIV - x)" by auto
   also have "\<dots> \<in> sigma_sets UNIV (Collect open)"
-    by (rule sigma_sets.Compl)
-       (auto intro!: sigma_sets.Basic simp: `closed x`)
+    by (force intro: sigma_sets.Compl simp: `closed x`)
   finally show "x \<in> sigma_sets UNIV (Collect open)" by simp
 qed simp_all
 
@@ -1151,14 +1151,10 @@
   fixes f :: "'a \<Rightarrow> ereal" 
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
-proof -
-  have "(\<lambda>x. if f x \<in> UNIV - { \<infinity>, - \<infinity> } then real (f x) else 0) \<in> borel_measurable M"
-    using continuous_on_real
-    by (rule borel_measurable_continuous_on_open[OF _ _ f]) auto
-  also have "(\<lambda>x. if f x \<in> UNIV - { \<infinity>, - \<infinity> } then real (f x) else 0) = (\<lambda>x. real (f x))"
-    by auto
-  finally show ?thesis .
-qed
+  apply (rule measurable_compose[OF f])
+  apply (rule borel_measurable_continuous_countable_exceptions[of "{\<infinity>, -\<infinity> }"])
+  apply (auto intro: continuous_on_real simp: Compl_eq_Diff_UNIV)
+  done
 
 lemma borel_measurable_ereal_cases:
   fixes f :: "'a \<Rightarrow> ereal" 
@@ -1229,83 +1225,31 @@
   finally show "f \<in> borel_measurable M" .
 qed simp_all
 
-lemma borel_measurable_eq_atMost_ereal:
-  fixes f :: "'a \<Rightarrow> ereal"
-  shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)"
-proof (intro iffI allI)
-  assume pos[rule_format]: "\<forall>a. f -` {..a} \<inter> space M \<in> sets M"
-  show "f \<in> borel_measurable M"
-    unfolding borel_measurable_ereal_iff_real borel_measurable_iff_le
-  proof (intro conjI allI)
-    fix a :: real
-    { fix x :: ereal assume *: "\<forall>i::nat. real i < x"
-      have "x = \<infinity>"
-      proof (rule ereal_top)
-        fix B from reals_Archimedean2[of B] guess n ..
-        then have "ereal B < real n" by auto
-        with * show "B \<le> x" by (metis less_trans less_imp_le)
-      qed }
-    then have "f -` {\<infinity>} \<inter> space M = space M - (\<Union>i::nat. f -` {.. real i} \<inter> space M)"
-      by (auto simp: not_le)
-    then show "f -` {\<infinity>} \<inter> space M \<in> sets M" using pos
-      by (auto simp del: UN_simps)
-    moreover
-    have "{-\<infinity>::ereal} = {..-\<infinity>}" by auto
-    then show "f -` {-\<infinity>} \<inter> space M \<in> sets M" using pos by auto
-    moreover have "{x\<in>space M. f x \<le> ereal a} \<in> sets M"
-      using pos[of "ereal a"] by (simp add: vimage_def Int_def conj_commute)
-    moreover have "{w \<in> space M. real (f w) \<le> a} =
-      (if a < 0 then {w \<in> space M. f w \<le> ereal a} - f -` {-\<infinity>} \<inter> space M
-      else {w \<in> space M. f w \<le> ereal a} \<union> (f -` {\<infinity>} \<inter> space M) \<union> (f -` {-\<infinity>} \<inter> space M))" (is "?l = ?r")
-      proof (intro set_eqI) fix x show "x \<in> ?l \<longleftrightarrow> x \<in> ?r" by (cases "f x") auto qed
-    ultimately show "{w \<in> space M. real (f w) \<le> a} \<in> sets M" by auto
-  qed
-qed (simp add: measurable_sets)
+lemma borel_measurable_ereal_iff_Iio:
+  "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..< a} \<inter> space M \<in> sets M)"
+  by (auto simp: borel_Iio measurable_iff_measure_of)
+
+lemma borel_measurable_ereal_iff_Ioi:
+  "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a <..} \<inter> space M \<in> sets M)"
+  by (auto simp: borel_Ioi measurable_iff_measure_of)
 
-lemma borel_measurable_eq_atLeast_ereal:
-  "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a..} \<inter> space M \<in> sets M)"
-proof
-  assume pos: "\<forall>a. f -` {a..} \<inter> space M \<in> sets M"
-  moreover have "\<And>a. (\<lambda>x. - f x) -` {..a} = f -` {-a ..}"
-    by (auto simp: ereal_uminus_le_reorder)
-  ultimately have "(\<lambda>x. - f x) \<in> borel_measurable M"
-    unfolding borel_measurable_eq_atMost_ereal by auto
-  then show "f \<in> borel_measurable M" by simp
-qed (simp add: measurable_sets)
-
-lemma greater_eq_le_measurable:
-  fixes f :: "'a \<Rightarrow> 'c::linorder"
-  shows "f -` {..< a} \<inter> space M \<in> sets M \<longleftrightarrow> f -` {a ..} \<inter> space M \<in> sets M"
-proof
-  assume "f -` {a ..} \<inter> space M \<in> sets M"
-  moreover have "f -` {..< a} \<inter> space M = space M - f -` {a ..} \<inter> space M" by auto
-  ultimately show "f -` {..< a} \<inter> space M \<in> sets M" by auto
-next
-  assume "f -` {..< a} \<inter> space M \<in> sets M"
-  moreover have "f -` {a ..} \<inter> space M = space M - f -` {..< a} \<inter> space M" by auto
-  ultimately show "f -` {a ..} \<inter> space M \<in> sets M" by auto
+lemma vimage_sets_compl_iff:
+  "f -` A \<inter> space M \<in> sets M \<longleftrightarrow> f -` (- A) \<inter> space M \<in> sets M"
+proof -
+  { fix A assume "f -` A \<inter> space M \<in> sets M"
+    moreover have "f -` (- A) \<inter> space M = space M - f -` A \<inter> space M" by auto
+    ultimately have "f -` (- A) \<inter> space M \<in> sets M" by auto }
+  from this[of A] this[of "-A"] show ?thesis
+    by (metis double_complement)
 qed
 
-lemma borel_measurable_ereal_iff_less:
-  "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..< a} \<inter> space M \<in> sets M)"
-  unfolding borel_measurable_eq_atLeast_ereal greater_eq_le_measurable ..
+lemma borel_measurable_iff_Iic_ereal:
+  "(f::'a\<Rightarrow>ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)"
+  unfolding borel_measurable_ereal_iff_Ioi vimage_sets_compl_iff[where A="{a <..}" for a] by simp
 
-lemma less_eq_ge_measurable:
-  fixes f :: "'a \<Rightarrow> 'c::linorder"
-  shows "f -` {a <..} \<inter> space M \<in> sets M \<longleftrightarrow> f -` {..a} \<inter> space M \<in> sets M"
-proof
-  assume "f -` {a <..} \<inter> space M \<in> sets M"
-  moreover have "f -` {..a} \<inter> space M = space M - f -` {a <..} \<inter> space M" by auto
-  ultimately show "f -` {..a} \<inter> space M \<in> sets M" by auto
-next
-  assume "f -` {..a} \<inter> space M \<in> sets M"
-  moreover have "f -` {a <..} \<inter> space M = space M - f -` {..a} \<inter> space M" by auto
-  ultimately show "f -` {a <..} \<inter> space M \<in> sets M" by auto
-qed
-
-lemma borel_measurable_ereal_iff_ge:
-  "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a <..} \<inter> space M \<in> sets M)"
-  unfolding borel_measurable_eq_atMost_ereal less_eq_ge_measurable ..
+lemma borel_measurable_iff_Ici_ereal:
+  "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {a..} \<inter> space M \<in> sets M)"
+  unfolding borel_measurable_ereal_iff_Iio vimage_sets_compl_iff[where A="{..< a}" for a] by simp
 
 lemma borel_measurable_ereal2:
   fixes f g :: "'a \<Rightarrow> ereal" 
@@ -1352,20 +1296,13 @@
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
-proof cases
-  assume "finite S"
-  thus ?thesis using assms
-    by induct auto
-qed simp
+  using assms by (induction S rule: infinite_finite_induct) auto
 
 lemma borel_measurable_ereal_setprod[measurable (raw)]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
-proof cases
-  assume "finite S"
-  thus ?thesis using assms by induct auto
-qed simp
+  using assms by (induction S rule: infinite_finite_induct) auto
 
 lemma [measurable (raw)]:
   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
diff -r 2f5447b764f9 -r e6acec6a6f6f src/HOL/Probability/Measurable.thy
--- a/src/HOL/Probability/Measurable.thy	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/HOL/Probability/Measurable.thy	Thu Jan 15 21:45:23 2015 +0100
@@ -97,6 +97,7 @@
 
 declare measurable_cong_sets[measurable_cong]
 declare sets_restrict_space_cong[measurable_cong]
+declare sets_restrict_UNIV[measurable_cong]
 
 lemma predE[measurable (raw)]: 
   "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"
diff -r 2f5447b764f9 -r e6acec6a6f6f src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu Jan 15 21:45:23 2015 +0100
@@ -2440,6 +2440,9 @@
     by simp
 qed
 
+lemma sets_restrict_UNIV[simp]: "sets (restrict_space M UNIV) = sets M"
+  by (auto simp add: sets_restrict_space)
+
 lemma sets_restrict_space_iff:
   "\<Omega> \<inter> space M \<in> sets M \<Longrightarrow> A \<in> sets (restrict_space M \<Omega>) \<longleftrightarrow> (A \<subseteq> \<Omega> \<and> A \<in> sets M)"
 proof (subst sets_restrict_space, safe)
@@ -2525,5 +2528,40 @@
     by (auto simp add: sets_restrict_space_iff space_restrict_space)
 qed
 
+lemma measurableI:
+  "(\<And>x. x \<in> space M \<Longrightarrow> f x \<in> space N) \<Longrightarrow>
+    (\<And>A. A \<in> sets N \<Longrightarrow> f -` A \<inter> space M \<in> sets M) \<Longrightarrow>
+    f \<in> measurable M N"
+  by (auto simp: measurable_def)
+
+lemma measurable_piecewise_restrict:
+  assumes I: "countable I" and X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets M" "(\<Union>i\<in>I. X i) = space M"
+    and meas: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> measurable (restrict_space M (X i)) N"
+    and eq: "\<And>i x. i \<in> I \<Longrightarrow> x \<in> X i \<Longrightarrow> f i x = f' x"
+  shows "f' \<in> measurable M N"
+proof (rule measurableI)
+  fix x assume "x \<in> space M"
+  then obtain i where "i \<in> I" "x \<in> X i"
+    using X by auto
+  then show "f' x \<in> space N"
+    using eq[of i x] meas[THEN measurable_space, of i x] `x \<in> space M`
+    by (auto simp: space_restrict_space)
+next
+  fix A assume A: "A \<in> sets N"
+  have "f' -` A \<inter> space M = {x \<in> space M. \<forall>i\<in>I. x \<in> X i \<longrightarrow> f i x \<in> A}"
+    by (auto simp: eq X(2)[symmetric])
+  also have "\<dots> \<in> sets M"
+  proof (intro sets.sets_Collect_countable_All'[OF _ I])
+    fix i assume "i \<in> I"
+    then have "(f i -` A \<inter> X i) \<union> (space M - X i) \<in> sets M"
+      using meas[THEN measurable_sets, OF `i \<in> I` A] X(1)
+      by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
+    also have "(f i -` A \<inter> X i) \<union> (space M - X i) = {x \<in> space M. x \<in> X i \<longrightarrow> f i x \<in> A}"
+      using `i \<in> I` by (auto simp: X(2)[symmetric])
+    finally show "{x \<in> space M. x \<in> X i \<longrightarrow> f i x \<in> A} \<in> sets M" .
+  qed
+  finally show "f' -` A \<inter> space M \<in> sets M" .
+qed
+
 end
 
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/Concurrent/future.scala
--- a/src/Pure/Concurrent/future.scala	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/Pure/Concurrent/future.scala	Thu Jan 15 21:45:23 2015 +0100
@@ -47,6 +47,7 @@
 
 trait Promise[A] extends Future[A]
 {
+  def cancel: Unit
   def fulfill_result(res: Exn.Result[A]): Unit
   def fulfill(x: A): Unit
 }
@@ -78,6 +79,10 @@
 {
   override def is_finished: Boolean = promise.isCompleted
 
+  def cancel: Unit =
+    try { fulfill_result(Exn.Exn(Exn.Interrupt())) }
+    catch { case _: IllegalStateException => }
+
   def fulfill_result(res: Exn.Result[A]): Unit =
     res match {
       case Exn.Res(x) => promise.success(x)
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/Pure/General/path.ML	Thu Jan 15 21:45:23 2015 +0100
@@ -23,6 +23,7 @@
   val make: string list -> T
   val implode: T -> string
   val explode: string -> T
+  val decode: T XML.Decode.T
   val split: string -> T list
   val pretty: T -> Pretty.T
   val print: T -> string
@@ -161,6 +162,8 @@
   space_explode ":" str
   |> map_filter (fn s => if s = "" then NONE else SOME (explode_path s));
 
+val decode = XML.Decode.string #> explode_path;
+
 
 (* print *)
 
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/PIDE/batch_session.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/batch_session.scala	Thu Jan 15 21:45:23 2015 +0100
@@ -0,0 +1,72 @@
+/*  Title:      Pure/Tools/batch_session.scala
+    Author:     Makarius
+
+PIDE session in batch mode.
+*/
+
+package isabelle
+
+
+import isabelle._
+
+
+object Batch_Session
+{
+  def batch_session(
+    options: Options,
+    verbose: Boolean = false,
+    dirs: List[Path] = Nil,
+    session: String): Batch_Session =
+  {
+    val (_, session_tree) =
+      Build.find_sessions(options, dirs).selection(false, false, Nil, List(session))
+    val session_info = session_tree(session)
+    val parent_session =
+      session_info.parent getOrElse error("No parent session for " + quote(session))
+
+    if (Build.build(options, new Build.Console_Progress(verbose),
+        verbose = verbose, build_heap = true,
+        dirs = dirs, sessions = List(parent_session)) != 0)
+      new RuntimeException
+
+    val deps = Build.dependencies(Build.Ignore_Progress, false, verbose, false, session_tree)
+    val resources =
+    {
+      val content = deps(parent_session)
+      new Resources(content.loaded_theories, content.known_theories, content.syntax)
+    }
+
+    val progress = new Build.Console_Progress(verbose)
+
+    val prover_session = new Session(resources)
+    val batch_session = new Batch_Session(prover_session)
+
+    val handler = new Build.Handler(progress, session)
+
+    prover_session.phase_changed +=
+      Session.Consumer[Session.Phase](getClass.getName) {
+        case Session.Ready =>
+          prover_session.add_protocol_handler(handler)
+          val master_dir = session_info.dir
+          val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) })
+          batch_session.build_theories_result =
+            Some(Build.build_theories(prover_session, master_dir, theories))
+        case Session.Inactive | Session.Failed =>
+          batch_session.session_result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
+        case Session.Shutdown =>
+          batch_session.session_result.fulfill(())
+        case _ =>
+      }
+
+    prover_session.start("Isabelle", List("-r", "-q", parent_session))
+
+    batch_session
+  }
+}
+
+class Batch_Session private(val session: Session)
+{
+  val session_result = Future.promise[Unit]
+  @volatile var build_theories_result: Option[Promise[XML.Body]] = None
+}
+
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Jan 15 21:45:23 2015 +0100
@@ -245,12 +245,14 @@
     val get_blob: Option[Document.Blob] = None,
     val header: Node.Header = Node.no_header,
     val syntax: Option[Prover.Syntax] = None,
+    val text_perspective: Text.Perspective = Text.Perspective.empty,
     val perspective: Node.Perspective_Command = Node.no_perspective_command,
     _commands: Node.Commands = Node.Commands.empty)
   {
     def is_empty: Boolean =
       get_blob.isEmpty &&
       header == Node.no_header &&
+      text_perspective.is_empty &&
       Node.is_no_perspective_command(perspective) &&
       commands.isEmpty
 
@@ -262,22 +264,32 @@
     def init_blob(blob: Document.Blob): Node = new Node(get_blob = Some(blob.unchanged))
 
     def update_header(new_header: Node.Header): Node =
-      new Node(get_blob, new_header, syntax, perspective, _commands)
+      new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands)
 
     def update_syntax(new_syntax: Option[Prover.Syntax]): Node =
-      new Node(get_blob, header, new_syntax, perspective, _commands)
+      new Node(get_blob, header, new_syntax, text_perspective, perspective, _commands)
+
+    def update_perspective(
+        new_text_perspective: Text.Perspective,
+        new_perspective: Node.Perspective_Command): Node =
+      new Node(get_blob, header, syntax, new_text_perspective, new_perspective, _commands)
 
-    def update_perspective(new_perspective: Node.Perspective_Command): Node =
-      new Node(get_blob, header, syntax, new_perspective, _commands)
+    def edit_perspective: Node.Edit[Text.Edit, Text.Perspective] =
+      Node.Perspective(perspective.required, text_perspective, perspective.overlays)
 
-    def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
+    def same_perspective(
+        other_text_perspective: Text.Perspective,
+        other_perspective: Node.Perspective_Command): Boolean =
+      text_perspective == other_text_perspective &&
       perspective.required == other_perspective.required &&
       perspective.visible.same(other_perspective.visible) &&
       perspective.overlays == other_perspective.overlays
 
     def update_commands(new_commands: Linear_Set[Command]): Node =
       if (new_commands eq _commands.commands) this
-      else new Node(get_blob, header, syntax, perspective, Node.Commands(new_commands))
+      else
+        new Node(get_blob, header, syntax, text_perspective, perspective,
+          Node.Commands(new_commands))
 
     def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
       _commands.iterator(i)
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu Jan 15 21:45:23 2015 +0100
@@ -186,7 +186,7 @@
   val command_timing: Properties.entry
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
-  val use_theories_result: string -> bool -> Properties.T
+  val build_theories_result: string -> Properties.T
   val print_operationsN: string
   val print_operations: Properties.T
   val simp_trace_panelN: string
@@ -597,8 +597,7 @@
 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
   | dest_loading_theory _ = NONE;
 
-fun use_theories_result id ok =
-  [("function", "use_theories_result"), ("id", id), ("ok", print_bool ok)];
+fun build_theories_result id = [("function", "build_theories_result"), ("id", id)];
 
 val print_operationsN = "print_operations";
 val print_operations = [(functionN, print_operationsN)];
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/Pure/PIDE/markup.scala	Thu Jan 15 21:45:23 2015 +0100
@@ -458,21 +458,22 @@
       }
   }
 
+  val LOADING_THEORY = "loading_theory"
   object Loading_Theory
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
-        case List((FUNCTION, "loading_theory"), (NAME, name)) => Some(name)
+        case List((FUNCTION, LOADING_THEORY), (NAME, name)) => Some(name)
         case _ => None
       }
   }
 
-  object Use_Theories_Result
+  val BUILD_THEORIES_RESULT = "build_theories_result"
+  object Build_Theories_Result
   {
-    def unapply(props: Properties.T): Option[(String, Boolean)] =
+    def unapply(props: Properties.T): Option[String] =
       props match {
-        case List((FUNCTION, "use_theories_result"),
-          ("id", id), ("ok", Properties.Value.Boolean(ok))) => Some((id, ok))
+        case List((FUNCTION, BUILD_THEORIES_RESULT), ("id", id)) => Some(id)
         case _ => None
       }
   }
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/Pure/PIDE/protocol.ML	Thu Jan 15 21:45:23 2015 +0100
@@ -53,45 +53,46 @@
 
 val _ =
   Isabelle_Process.protocol_command "Document.update"
-    (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
-      let
-        val _ = Execution.discontinue ();
+    (Future.task_context "Document.update" (Future.new_group NONE)
+      (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
+        let
+          val _ = Execution.discontinue ();
 
-        val old_id = Document_ID.parse old_id_string;
-        val new_id = Document_ID.parse new_id_string;
-        val edits =
-          YXML.parse_body edits_yxml |>
-            let open XML.Decode in
-              list (pair string
-                (variant
-                 [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
-                  fn ([], a) =>
-                    let
-                      val (master, (name, (imports, (keywords, errors)))) =
-                        pair string (pair string (pair (list string)
-                          (pair (list (pair string
-                            (option (pair (pair string (list string)) (list string)))))
-                            (list string)))) a;
-                      val imports' = map (rpair Position.none) imports;
-                      val header = Thy_Header.make (name, Position.none) imports' keywords;
-                    in Document.Deps (master, header, errors) end,
-                  fn (a :: b, c) =>
-                    Document.Perspective (bool_atom a, map int_atom b,
-                      list (pair int (pair string (list string))) c)]))
-            end;
+          val old_id = Document_ID.parse old_id_string;
+          val new_id = Document_ID.parse new_id_string;
+          val edits =
+            YXML.parse_body edits_yxml |>
+              let open XML.Decode in
+                list (pair string
+                  (variant
+                   [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
+                    fn ([], a) =>
+                      let
+                        val (master, (name, (imports, (keywords, errors)))) =
+                          pair string (pair string (pair (list string)
+                            (pair (list (pair string
+                              (option (pair (pair string (list string)) (list string)))))
+                              (list string)))) a;
+                        val imports' = map (rpair Position.none) imports;
+                        val header = Thy_Header.make (name, Position.none) imports' keywords;
+                      in Document.Deps (master, header, errors) end,
+                    fn (a :: b, c) =>
+                      Document.Perspective (bool_atom a, map int_atom b,
+                        list (pair int (pair string (list string))) c)]))
+              end;
 
-        val (removed, assign_update, state') = Document.update old_id new_id edits state;
-        val _ = List.app Execution.terminate removed;
-        val _ = Execution.purge removed;
-        val _ = List.app Isabelle_Process.reset_tracing removed;
+          val (removed, assign_update, state') = Document.update old_id new_id edits state;
+          val _ = List.app Execution.terminate removed;
+          val _ = Execution.purge removed;
+          val _ = List.app Isabelle_Process.reset_tracing removed;
 
-        val _ =
-          Output.protocol_message Markup.assign_update
-            [(new_id, assign_update) |>
-              let open XML.Encode
-              in pair int (list (pair int (list int))) end
-              |> YXML.string_of_body];
-      in Document.start_execution state' end));
+          val _ =
+            Output.protocol_message Markup.assign_update
+              [(new_id, assign_update) |>
+                let open XML.Encode
+                in pair int (list (pair int (list int))) end
+                |> YXML.string_of_body];
+        in Document.start_execution state' end)));
 
 val _ =
   Isabelle_Process.protocol_command "Document.remove_versions"
@@ -111,21 +112,6 @@
         handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn);
 
 val _ =
-  Isabelle_Process.protocol_command "use_theories"
-    (fn id :: master_dir :: thys =>
-      let
-        val result =
-          Exn.capture (fn () =>
-            Thy_Info.use_theories
-              {document = false, last_timing = K NONE, master_dir = Path.explode master_dir}
-              (map (rpair Position.none) thys)) ();
-        val ok =
-          (case result of
-            Exn.Res _ => true
-          | Exn.Exn exn => (Runtime.exn_error_message exn; false));
-    in Output.protocol_message (Markup.use_theories_result id ok) [] end);
-
-val _ =
   Isabelle_Process.protocol_command "ML_System.share_common_data"
     (fn [] => ML_System.share_common_data ());
 
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/Pure/PIDE/protocol.scala	Thu Jan 15 21:45:23 2015 +0100
@@ -456,8 +456,8 @@
   def remove_versions(versions: List[Document.Version])
   {
     val versions_yxml =
-      { import XML.Encode._
-        YXML.string_of_body(list(long)(versions.map(_.id))) }
+    { import XML.Encode._
+      YXML.string_of_body(list(long)(versions.map(_.id))) }
     protocol_command("Document.remove_versions", versions_yxml)
   }
 
@@ -468,8 +468,13 @@
     protocol_command("Document.dialog_result", Properties.Value.Long(serial), result)
 
 
-  /* use_theories */
+  /* build_theories */
 
-  def use_theories(id: String, master_dir: Path, thys: List[Path]): Unit =
-    protocol_command("use_theories", (id :: master_dir.implode :: thys.map(_.implode)): _*)
+  def build_theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
+  {
+    val theories_yxml =
+    { import XML.Encode._
+      YXML.string_of_body(list(pair(Options.encode, list(Path.encode)))(theories)) }
+    protocol_command("build_theories", id, master_dir.implode, theories_yxml)
+  }
 }
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/PIDE/session.ML
--- a/src/Pure/PIDE/session.ML	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/Pure/PIDE/session.ML	Thu Jan 15 21:45:23 2015 +0100
@@ -11,6 +11,7 @@
   val get_keywords: unit -> Keyword.keywords
   val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     (Path.T * Path.T) list -> string -> string * string -> bool -> unit
+  val shutdown: unit -> unit
   val finish: unit -> unit
   val save: string -> unit
   val protocol_handler: string -> unit
@@ -58,22 +59,23 @@
 
 (* finish *)
 
+fun shutdown () =
+ (Execution.shutdown ();
+  Event_Timer.shutdown ();
+  Future.shutdown ());
+
 fun finish () =
- (Execution.shutdown ();
+ (shutdown ();
   Thy_Info.finish ();
   Present.finish ();
-  Future.shutdown ();
-  Event_Timer.shutdown ();
-  Future.shutdown ();
+  shutdown ();
   keywords :=
     fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory)
       (Thy_Info.get_names ()) Keyword.empty_keywords;
   session_finished := true);
 
 fun save heap =
- (Execution.shutdown ();
-  Event_Timer.shutdown ();
-  Future.shutdown ();
+ (shutdown ();
   ML_System.share_common_data ();
   ML_System.save_state heap);
 
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/Pure/PIDE/session.scala	Thu Jan 15 21:45:23 2015 +0100
@@ -63,6 +63,7 @@
   case object Caret_Focus
   case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
+  case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
   case class Commands_Changed(
     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
 
@@ -104,14 +105,20 @@
     val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
   }
 
-  class Protocol_Handlers(
+  def bad_protocol_handler(exn: Throwable, name: String): Unit =
+    Output.error_message(
+      "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
+
+  private class Protocol_Handlers(
     handlers: Map[String, Session.Protocol_Handler] = Map.empty,
     functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
   {
     def get(name: String): Option[Protocol_Handler] = handlers.get(name)
 
-    def add(prover: Prover, name: String): Protocol_Handlers =
+    def add(prover: Prover, handler: Protocol_Handler): Protocol_Handlers =
     {
+      val name = handler.getClass.getName
+
       val (handlers1, functions1) =
         handlers.get(name) match {
           case Some(old_handler) =>
@@ -123,22 +130,20 @@
 
       val (handlers2, functions2) =
         try {
-          val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
-          new_handler.start(prover)
+          handler.start(prover)
 
           val new_functions =
-            for ((a, f) <- new_handler.functions.toList) yield
+            for ((a, f) <- handler.functions.toList) yield
               (a, (msg: Prover.Protocol_Output) => f(prover, msg))
 
           val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
           if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
 
-          (handlers1 + (name -> new_handler), functions1 ++ new_functions)
+          (handlers1 + (name -> handler), functions1 ++ new_functions)
         }
         catch {
           case exn: Throwable =>
-            Output.error_message(
-              "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
+            Session.bad_protocol_handler(exn, name)
             (handlers1, functions1)
         }
 
@@ -236,14 +241,6 @@
     resources.base_syntax
 
 
-  /* protocol handlers */
-
-  @volatile private var _protocol_handlers = new Session.Protocol_Handlers()
-
-  def protocol_handler(name: String): Option[Session.Protocol_Handler] =
-    _protocol_handlers.get(name)
-
-
   /* theory files */
 
   def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
@@ -342,6 +339,17 @@
   }
 
 
+  /* protocol handlers */
+
+  private val _protocol_handlers = Synchronized(new Session.Protocol_Handlers)
+
+  def get_protocol_handler(name: String): Option[Session.Protocol_Handler] =
+    _protocol_handlers.value.get(name)
+
+  def add_protocol_handler(handler: Session.Protocol_Handler): Unit =
+    _protocol_handlers.change(_.add(prover.get, handler))
+
+
   /* manager thread */
 
   private val delay_prune = Simple_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
@@ -431,11 +439,16 @@
 
       output match {
         case msg: Prover.Protocol_Output =>
-          val handled = _protocol_handlers.invoke(msg)
+          val handled = _protocol_handlers.value.invoke(msg)
           if (!handled) {
             msg.properties match {
               case Markup.Protocol_Handler(name) if prover.defined =>
-                _protocol_handlers = _protocol_handlers.add(prover.get, name)
+                try {
+                  val handler =
+                    Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]
+                  add_protocol_handler(handler)
+                }
+                catch { case exn: Throwable => Session.bad_protocol_handler(exn, name) }
 
               case Protocol.Command_Timing(state_id, timing) if prover.defined =>
                 val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
@@ -524,7 +537,7 @@
 
           case Stop =>
             if (prover.defined && is_ready) {
-              _protocol_handlers = _protocol_handlers.stop(prover.get)
+              _protocol_handlers.change(_.stop(prover.get))
               global_state.change(_ => Document.State.init)
               phase = Session.Shutdown
               prover.get.terminate
@@ -553,6 +566,9 @@
             prover.get.dialog_result(serial, result)
             handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
 
+          case Session.Build_Theories(id, master_dir, theories) if prover.defined =>
+            prover.get.build_theories(id, master_dir, theories)
+
           case Protocol_Command(name, args) if prover.defined =>
             prover.get.protocol_command(name, args:_*)
 
@@ -615,4 +631,7 @@
 
   def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
   { manager.send(Session.Dialog_Result(id, serial, result)) }
+
+  def build_theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
+  { manager.send(Session.Build_Theories(id, master_dir, theories)) }
 }
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/Pure/ROOT.ML	Thu Jan 15 21:45:23 2015 +0100
@@ -65,6 +65,7 @@
 use "General/linear_set.ML";
 use "General/buffer.ML";
 use "General/pretty.ML";
+use "PIDE/xml.ML";
 use "General/path.ML";
 use "General/url.ML";
 use "General/file.ML";
@@ -78,7 +79,6 @@
 if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
 use "General/sha1_samples.ML";
 
-use "PIDE/xml.ML";
 use "PIDE/yxml.ML";
 use "PIDE/document_id.ML";
 
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/Pure/System/isabelle_process.ML	Thu Jan 15 21:45:23 2015 +0100
@@ -162,9 +162,6 @@
   System_Channel.input_line channel
   |> Option.map (fn line => map (read_chunk channel) (space_explode "," line));
 
-fun task_context e =
-  Future.task_context "Isabelle_Process.loop" (Future.new_group NONE) e ();
-
 in
 
 fun loop channel =
@@ -173,7 +170,7 @@
       (case read_command channel of
         NONE => false
       | SOME [] => (Output.system_message "Isabelle process: no input"; true)
-      | SOME (name :: args) => (task_context (fn () => run_command name args); true))
+      | SOME (name :: args) => (run_command name args; true))
       handle exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
   in
     if continue then loop channel
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/Thy/thy_info.ML
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Jan 15 21:45:23 2015 +0100
@@ -288,11 +288,12 @@
         val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays)
         val perspective: Document.Node.Perspective_Command =
           Document.Node.Perspective(required, visible_overlay, overlays)
-        if (node.same_perspective(perspective)) node
+        if (node.same_perspective(text_perspective, perspective)) node
         else
-          node.update_perspective(perspective).update_commands(
-            consolidate_spans(resources, syntax, get_blob, reparse_limit,
-              name, visible, node.commands))
+          node.update_perspective(text_perspective, perspective).
+            update_commands(
+              consolidate_spans(resources, syntax, get_blob, reparse_limit,
+                name, visible, node.commands))
     }
   }
 
@@ -341,13 +342,18 @@
               else node
             val node2 =
               (node1 /: edits)(text_edit(resources, syntax, get_blob, reparse_limit, _, _))
-
-            if (!(node.same_perspective(node2.perspective)))
-              doc_edits += (name -> node2.perspective)
+            val node3 =
+              if (reparse_set.contains(name))
+                text_edit(resources, syntax, get_blob, reparse_limit,
+                  node2, (name, node2.edit_perspective))
+              else node2
 
-            doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
+            if (!(node.same_perspective(node3.text_perspective, node3.perspective)))
+              doc_edits += (name -> node3.perspective)
 
-            nodes += (name -> node2)
+            doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node3.commands)))
+
+            nodes += (name -> node3)
         }
         (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(nodes))
       }
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/Pure/Tools/build.ML	Thu Jan 15 21:45:23 2015 +0100
@@ -97,33 +97,28 @@
 
 (* build *)
 
-local
-
-fun use_theories last_timing options =
-  Thy_Info.use_theories {
-      document = Present.document_enabled (Options.string options "document"),
-      last_timing = last_timing,
-      master_dir = Path.current}
-    |> Unsynchronized.setmp print_mode
-        (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
-    |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
-    |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
-    |> Multithreading.max_threads_setmp (Options.int options "threads")
-    |> Unsynchronized.setmp Future.ML_statistics true;
-
-fun use_theories_condition last_timing (options, thys) =
-  let val condition = space_explode "," (Options.string options "condition") in
-    (case filter_out (can getenv_strict) condition of
-      [] =>
-        (Options.set_default options;
-         use_theories last_timing options (map (rpair Position.none) thys))
-    | conds =>
-        Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
-          " (undefined " ^ commas conds ^ ")\n"))
+fun build_theories last_timing master_dir (options, thys) =
+  let
+    val condition = space_explode "," (Options.string options "condition");
+    val conds = filter_out (can getenv_strict) condition;
+  in
+    if null conds then
+      (Options.set_default options;
+        (Thy_Info.use_theories {
+          document = Present.document_enabled (Options.string options "document"),
+          last_timing = last_timing,
+          master_dir = master_dir}
+        |> Unsynchronized.setmp print_mode
+            (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
+        |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
+        |> Multithreading.max_threads_setmp (Options.int options "threads")
+        |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
+        |> Unsynchronized.setmp Future.ML_statistics true) thys)
+    else
+      Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
+        " (undefined " ^ commas conds ^ ")\n")
   end;
 
-in
-
 fun build args_file = Command_Line.tool0 (fn () =>
     let
       val _ = SHA1_Samples.test ();
@@ -134,7 +129,7 @@
           let open XML.Decode in
             pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
               (pair (list (pair string string)) (pair string (pair string (pair string
-                ((list (pair Options.decode (list string))))))))))))
+                ((list (pair Options.decode (list (string #> rpair Position.none)))))))))))))
           end;
 
       val _ = Options.set_default options;
@@ -156,7 +151,7 @@
 
       val res1 =
         theories |>
-          (List.app (use_theories_condition last_timing)
+          (List.app (build_theories last_timing Path.current)
             |> session_timing name verbose
             |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
             |> Multithreading.max_threads_setmp (Options.int options "threads")
@@ -168,6 +163,25 @@
       val _ = if do_output then () else exit 0;
     in () end);
 
-end;
+
+(* PIDE protocol *)
+
+val _ =
+  Isabelle_Process.protocol_command "build_theories"
+    (fn [id, master_dir, theories_yxml] =>
+      let
+        val theories =
+          YXML.parse_body theories_yxml |>
+            let open XML.Decode
+            in list (pair Options.decode (list (string #> rpair Position.none))) end;
+        val res1 =
+          Exn.capture (fn () =>
+            theories |> List.app (build_theories (K NONE) (Path.explode master_dir))) ();
+        val res2 = Exn.capture Session.shutdown ();
+        val result =
+          (Par_Exn.release_all [res1, res2]; "") handle exn =>
+            (Runtime.exn_message exn handle _ (*sic!*) =>
+              "Exception raised, but failed to print details!");
+    in Output.protocol_message (Markup.build_theories_result id) [result] end);
 
 end;
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/Pure/Tools/build.scala	Thu Jan 15 21:45:23 2015 +0100
@@ -1025,5 +1025,61 @@
       }
     }
   }
+
+
+  /* PIDE protocol */
+
+  def build_theories(
+    session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[XML.Body] =
+      session.get_protocol_handler(classOf[Handler].getName) match {
+        case Some(handler: Handler) => handler.build_theories(session, master_dir, theories)
+        case _ => error("Cannot invoke build_theories: bad protocol handler")
+      }
+
+  class Handler(progress: Progress, session_name: String) extends Session.Protocol_Handler
+  {
+    private val pending = Synchronized(Map.empty[String, Promise[XML.Body]])
+
+    def build_theories(
+      session: Session, master_dir: Path, theories: List[(Options, List[Path])]): Promise[XML.Body] =
+    {
+      val promise = Future.promise[XML.Body]
+      val id = Document_ID.make().toString
+      pending.change(promises => promises + (id -> promise))
+      session.build_theories(id, master_dir, theories)
+      promise
+    }
+
+    private def loading_theory(prover: Prover, msg: Prover.Protocol_Output): Boolean =
+      msg.properties match {
+        case Markup.Loading_Theory(name) => progress.theory(session_name, name); true
+        case _ => false
+      }
+
+    private def build_theories_result(prover: Prover, msg: Prover.Protocol_Output): Boolean =
+      msg.properties match {
+        case Markup.Build_Theories_Result(id) =>
+          pending.change_result(promises =>
+            promises.get(id) match {
+              case Some(promise) =>
+                val error_message =
+                  try { YXML.parse_body(Symbol.decode(msg.text)) }
+                  catch { case exn: Throwable => List(XML.Text(Exn.message(exn))) }
+                promise.fulfill(error_message)
+                (true, promises - id)
+              case None =>
+                (false, promises)
+            })
+        case _ => false
+      }
+
+    override def stop(prover: Prover): Unit =
+      pending.change(promises => { for ((_, promise) <- promises) promise.cancel; Map.empty })
+
+    val functions =
+      Map(
+        Markup.BUILD_THEORIES_RESULT -> build_theories_result _,
+        Markup.LOADING_THEORY -> loading_theory _)
+  }
 }
 
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/Tools/print_operation.scala
--- a/src/Pure/Tools/print_operation.scala	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/Pure/Tools/print_operation.scala	Thu Jan 15 21:45:23 2015 +0100
@@ -10,7 +10,7 @@
 object Print_Operation
 {
   def print_operations(session: Session): List[(String, String)] =
-    session.protocol_handler("isabelle.Print_Operation$Handler") match {
+    session.get_protocol_handler("isabelle.Print_Operation$Handler") match {
       case Some(handler: Handler) => handler.get
       case _ => Nil
     }
diff -r 2f5447b764f9 -r e6acec6a6f6f src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Jan 15 21:44:51 2015 +0100
+++ b/src/Pure/build-jars	Thu Jan 15 21:45:23 2015 +0100
@@ -55,6 +55,7 @@
   Isar/parse.scala
   Isar/token.scala
   ML/ml_lex.scala
+  PIDE/batch_session.scala
   PIDE/command.scala
   PIDE/command_span.scala
   PIDE/document.scala