--- 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
--- 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
--- 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"
--- 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"
--- 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
--- 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)
--- 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 *)
--- /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
+}
+
--- 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)
--- 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)];
--- 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
}
}
--- 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 ());
--- 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)
+ }
}
--- 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);
--- 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)) }
}
--- 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";
--- 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
--- 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))
}
--- 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;
--- 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 _)
+ }
}
--- 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
}
--- 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