--- a/src/HOL/Hahn_Banach/Function_Norm.thy Wed Jan 16 19:02:40 2013 +0100
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy Wed Jan 16 22:18:46 2013 +0100
@@ -244,7 +244,7 @@
lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
assumes "continuous V f norm"
- assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
+ assumes ineq: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
proof -
interpret continuous V f norm by fact
@@ -265,7 +265,7 @@
proof (rule mult_right_mono)
have "0 < \<parallel>x\<parallel>" using x x_neq ..
then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
- from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
+ from x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by (rule ineq)
qed
also have "\<dots> = c"
proof -
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Wed Jan 16 19:02:40 2013 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Wed Jan 16 22:18:46 2013 +0100
@@ -469,15 +469,13 @@
\end{center}
*}
- have "\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
+ from g_cont _ ge_zero
+ show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
proof
fix x assume "x \<in> E"
with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
by (simp only: p_def)
qed
- from g_cont this ge_zero
- show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
- by (rule fn_norm_least [of g, folded B_def fn_norm_def])
txt {* The other direction is achieved by a similar argument. *}
@@ -485,9 +483,9 @@
proof (rule normed_vectorspace_with_fn_norm.fn_norm_least
[OF normed_vectorspace_with_fn_norm.intro,
OF F_norm, folded B_def fn_norm_def])
- show "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
- proof
- fix x assume x: "x \<in> F"
+ fix x assume x: "x \<in> F"
+ show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
+ proof -
from a x have "g x = f x" ..
then have "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
also from g_cont
@@ -495,8 +493,9 @@
proof (rule fn_norm_le_cong [OF _ linearformE, folded B_def fn_norm_def])
from FE x show "x \<in> E" ..
qed
- finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" .
+ finally show ?thesis .
qed
+ next
show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
using g_cont
by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
--- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Jan 16 19:02:40 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Jan 16 22:18:46 2013 +0100
@@ -5868,165 +5868,378 @@
defer apply(rule insert(3)[OF False]) using insert(5) by auto
qed qed auto
+
subsection {* Dominated convergence. *}
-lemma dominated_convergence: fixes f::"nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
+lemma dominated_convergence:
+ fixes f :: "nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
assumes "\<And>k. (f k) integrable_on s" "h integrable_on s"
- "\<And>k. \<forall>x \<in> s. norm(f k x) \<le> (h x)"
- "\<forall>x \<in> s. ((\<lambda>k. f k x) ---> g x) sequentially"
- shows "g integrable_on s" "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
-proof- have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and>
+ "\<And>k. \<forall>x \<in> s. norm(f k x) \<le> (h x)"
+ "\<forall>x \<in> s. ((\<lambda>k. f k x) ---> g x) sequentially"
+ shows "g integrable_on s"
+ "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
+proof -
+ have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and>
((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) --->
integral s (\<lambda>x. Inf {f j x |j. m \<le> j}))sequentially"
- proof(rule monotone_convergence_decreasing,safe) fix m::nat
+ proof (rule monotone_convergence_decreasing, safe)
+ fix m :: nat
show "bounded {integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) |k. True}"
- unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
- proof safe fix k::nat
+ unfolding bounded_iff
+ apply (rule_tac x="integral s h" in exI)
+ proof safe
+ fix k :: nat
show "norm (integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
- apply(rule integral_norm_bound_integral) unfolding simple_image
- apply(rule absolutely_integrable_onD) apply(rule absolutely_integrable_inf_real)
- prefer 5 unfolding real_norm_def apply(rule) apply(rule Inf_abs_ge)
- prefer 5 apply rule apply(rule_tac g=h in absolutely_integrable_integrable_bound_real)
- using assms unfolding real_norm_def by auto
- qed fix k::nat show "(\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) integrable_on s"
- unfolding simple_image apply(rule absolutely_integrable_onD)
- apply(rule absolutely_integrable_inf_real) prefer 3
- using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)] by auto
- fix x assume x:"x\<in>s" show "Inf {f j x |j. j \<in> {m..m + Suc k}}
- \<le> Inf {f j x |j. j \<in> {m..m + k}}" apply(rule Inf_ge) unfolding setge_def
- defer apply rule apply(subst Inf_finite_le_iff) prefer 3
- apply(rule_tac x=xa in bexI) by auto
- let ?S = "{f j x| j. m \<le> j}" def i \<equiv> "Inf ?S"
+ apply (rule integral_norm_bound_integral)
+ unfolding simple_image
+ apply (rule absolutely_integrable_onD)
+ apply (rule absolutely_integrable_inf_real)
+ prefer 5
+ unfolding real_norm_def
+ apply rule
+ apply (rule Inf_abs_ge)
+ prefer 5
+ apply rule
+ apply (rule_tac g = h in absolutely_integrable_integrable_bound_real)
+ using assms
+ unfolding real_norm_def
+ apply auto
+ done
+ qed
+ fix k :: nat
+ show "(\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) integrable_on s"
+ unfolding simple_image
+ apply (rule absolutely_integrable_onD)
+ apply (rule absolutely_integrable_inf_real)
+ prefer 3
+ using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)]
+ apply auto
+ done
+ fix x
+ assume x: "x \<in> s"
+ show "Inf {f j x |j. j \<in> {m..m + Suc k}} \<le> Inf {f j x |j. j \<in> {m..m + k}}"
+ apply (rule Inf_ge)
+ unfolding setge_def
+ defer
+ apply rule
+ apply (subst Inf_finite_le_iff)
+ prefer 3
+ apply (rule_tac x=xa in bexI)
+ apply auto
+ done
+ let ?S = "{f j x| j. m \<le> j}"
+ def i \<equiv> "Inf ?S"
show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
- proof (rule LIMSEQ_I) case goal1 note r=this have i:"isGlb UNIV ?S i" unfolding i_def apply(rule Inf)
- defer apply(rule_tac x="- h x - 1" in exI) unfolding setge_def
- proof safe case goal1 thus ?case using assms(3)[rule_format,OF x, of j] by auto
+ proof (rule LIMSEQ_I)
+ case goal1
+ note r = this
+ have i: "isGlb UNIV ?S i"
+ unfolding i_def
+ apply (rule Inf)
+ defer
+ apply (rule_tac x="- h x - 1" in exI)
+ unfolding setge_def
+ proof safe
+ case goal1
+ thus ?case using assms(3)[rule_format,OF x, of j] by auto
qed auto
have "\<exists>y\<in>?S. \<not> y \<ge> i + r"
- proof(rule ccontr) case goal1 hence "i \<ge> i + r" apply-
- apply(rule isGlb_le_isLb[OF i]) apply(rule isLbI) unfolding setge_def by fastforce+
+ proof(rule ccontr)
+ case goal1
+ hence "i \<ge> i + r"
+ apply -
+ apply (rule isGlb_le_isLb[OF i])
+ apply (rule isLbI)
+ unfolding setge_def
+ apply fastforce+
+ done
thus False using r by auto
- qed then guess y .. note y=this[unfolded not_le]
+ qed
+ then guess y .. note y=this[unfolded not_le]
from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
- show ?case apply(rule_tac x=N in exI)
- proof safe case goal1
+ show ?case
+ apply (rule_tac x=N in exI)
+ proof safe
+ case goal1
have *:"\<And>y ix. y < i + r \<longrightarrow> i \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - i) < r" by arith
- show ?case unfolding real_norm_def apply(rule *[rule_format,OF y(2)])
- unfolding i_def apply(rule real_le_inf_subset) prefer 3
- apply(rule,rule isGlbD1[OF i]) prefer 3 apply(subst Inf_finite_le_iff)
- prefer 3 apply(rule_tac x=y in bexI) using N goal1 by auto
- qed qed qed note dec1 = conjunctD2[OF this]
+ show ?case
+ unfolding real_norm_def
+ apply (rule *[rule_format,OF y(2)])
+ unfolding i_def
+ apply (rule real_le_inf_subset)
+ prefer 3
+ apply (rule,rule isGlbD1[OF i])
+ prefer 3
+ apply (subst Inf_finite_le_iff)
+ prefer 3
+ apply (rule_tac x=y in bexI)
+ using N goal1
+ apply auto
+ done
+ qed
+ qed
+ qed
+ note dec1 = conjunctD2[OF this]
have "\<And>m. (\<lambda>x. Sup {f j x |j. m \<le> j}) integrable_on s \<and>
((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) --->
integral s (\<lambda>x. Sup {f j x |j. m \<le> j})) sequentially"
- proof(rule monotone_convergence_increasing,safe) fix m::nat
+ proof (rule monotone_convergence_increasing,safe)
+ fix m :: nat
show "bounded {integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) |k. True}"
- unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
- proof safe fix k::nat
+ unfolding bounded_iff
+ apply (rule_tac x="integral s h" in exI)
+ proof safe
+ fix k :: nat
show "norm (integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
- apply(rule integral_norm_bound_integral) unfolding simple_image
- apply(rule absolutely_integrable_onD) apply(rule absolutely_integrable_sup_real)
- prefer 5 unfolding real_norm_def apply(rule) apply(rule Sup_abs_le)
- prefer 5 apply rule apply(rule_tac g=h in absolutely_integrable_integrable_bound_real)
- using assms unfolding real_norm_def by auto
- qed fix k::nat show "(\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) integrable_on s"
- unfolding simple_image apply(rule absolutely_integrable_onD)
- apply(rule absolutely_integrable_sup_real) prefer 3
- using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)] by auto
- fix x assume x:"x\<in>s" show "Sup {f j x |j. j \<in> {m..m + Suc k}}
- \<ge> Sup {f j x |j. j \<in> {m..m + k}}" apply(rule Sup_le) unfolding setle_def
- defer apply rule apply(subst Sup_finite_ge_iff) prefer 3 apply(rule_tac x=y in bexI) by auto
- let ?S = "{f j x| j. m \<le> j}" def i \<equiv> "Sup ?S"
+ apply (rule integral_norm_bound_integral) unfolding simple_image
+ apply (rule absolutely_integrable_onD)
+ apply(rule absolutely_integrable_sup_real)
+ prefer 5 unfolding real_norm_def
+ apply rule
+ apply (rule Sup_abs_le)
+ prefer 5
+ apply rule
+ apply (rule_tac g=h in absolutely_integrable_integrable_bound_real)
+ using assms
+ unfolding real_norm_def
+ apply auto
+ done
+ qed
+ fix k :: nat
+ show "(\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) integrable_on s"
+ unfolding simple_image
+ apply (rule absolutely_integrable_onD)
+ apply (rule absolutely_integrable_sup_real)
+ prefer 3
+ using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)]
+ apply auto
+ done
+ fix x
+ assume x: "x\<in>s"
+ show "Sup {f j x |j. j \<in> {m..m + Suc k}} \<ge> Sup {f j x |j. j \<in> {m..m + k}}"
+ apply (rule Sup_le)
+ unfolding setle_def
+ defer
+ apply rule
+ apply (subst Sup_finite_ge_iff)
+ prefer 3
+ apply (rule_tac x=y in bexI)
+ apply auto
+ done
+ let ?S = "{f j x| j. m \<le> j}"
+ def i \<equiv> "Sup ?S"
show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
- proof (rule LIMSEQ_I) case goal1 note r=this have i:"isLub UNIV ?S i" unfolding i_def apply(rule Sup)
- defer apply(rule_tac x="h x" in exI) unfolding setle_def
- proof safe case goal1 thus ?case using assms(3)[rule_format,OF x, of j] by auto
+ proof (rule LIMSEQ_I)
+ case goal1 note r=this
+ have i: "isLub UNIV ?S i"
+ unfolding i_def
+ apply (rule Sup)
+ defer
+ apply (rule_tac x="h x" in exI)
+ unfolding setle_def
+ proof safe
+ case goal1
+ thus ?case using assms(3)[rule_format,OF x, of j] by auto
qed auto
have "\<exists>y\<in>?S. \<not> y \<le> i - r"
- proof(rule ccontr) case goal1 hence "i \<le> i - r" apply-
- apply(rule isLub_le_isUb[OF i]) apply(rule isUbI) unfolding setle_def by fastforce+
+ proof (rule ccontr)
+ case goal1
+ hence "i \<le> i - r"
+ apply -
+ apply (rule isLub_le_isUb[OF i])
+ apply (rule isUbI)
+ unfolding setle_def
+ apply fastforce+
+ done
thus False using r by auto
- qed then guess y .. note y=this[unfolded not_le]
+ qed
+ then guess y .. note y=this[unfolded not_le]
from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
- show ?case apply(rule_tac x=N in exI)
- proof safe case goal1
- have *:"\<And>y ix. i - r < y \<longrightarrow> ix \<le> i \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - i) < r" by arith
- show ?case unfolding real_norm_def apply(rule *[rule_format,OF y(2)])
- unfolding i_def apply(rule real_ge_sup_subset) prefer 3
- apply(rule,rule isLubD1[OF i]) prefer 3 apply(subst Sup_finite_ge_iff)
- prefer 3 apply(rule_tac x=y in bexI) using N goal1 by auto
- qed qed qed note inc1 = conjunctD2[OF this]
-
- have "g integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) ---> integral s g) sequentially"
- apply(rule monotone_convergence_increasing,safe) apply fact
- proof- show "bounded {integral s (\<lambda>x. Inf {f j x |j. k \<le> j}) |k. True}"
+ show ?case
+ apply (rule_tac x=N in exI)
+ proof safe
+ case goal1
+ have *: "\<And>y ix. i - r < y \<longrightarrow> ix \<le> i \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - i) < r"
+ by arith
+ show ?case
+ unfolding real_norm_def
+ apply (rule *[rule_format,OF y(2)])
+ unfolding i_def
+ apply (rule real_ge_sup_subset)
+ prefer 3
+ apply (rule, rule isLubD1[OF i])
+ prefer 3
+ apply (subst Sup_finite_ge_iff)
+ prefer 3
+ apply (rule_tac x = y in bexI)
+ using N goal1
+ apply auto
+ done
+ qed
+ qed
+ qed
+ note inc1 = conjunctD2[OF this]
+
+ have "g integrable_on s \<and>
+ ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) ---> integral s g) sequentially"
+ apply (rule monotone_convergence_increasing,safe)
+ apply fact
+ proof -
+ show "bounded {integral s (\<lambda>x. Inf {f j x |j. k \<le> j}) |k. True}"
unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
- proof safe fix k::nat
+ proof safe
+ fix k :: nat
show "norm (integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) \<le> integral s h"
- apply(rule integral_norm_bound_integral) apply fact+
- unfolding real_norm_def apply(rule) apply(rule Inf_abs_ge) using assms(3) by auto
- qed fix k::nat and x assume x:"x\<in>s"
-
- have *:"\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
- show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}" apply-
- apply(rule real_le_inf_subset) prefer 3 unfolding setge_def
- apply(rule_tac x="- h x" in exI) apply safe apply(rule *)
- using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
+ apply (rule integral_norm_bound_integral)
+ apply fact+
+ unfolding real_norm_def
+ apply rule
+ apply (rule Inf_abs_ge)
+ using assms(3)
+ apply auto
+ done
+ qed
+ fix k :: nat and x
+ assume x: "x \<in> s"
+
+ have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
+ show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}"
+ apply -
+ apply (rule real_le_inf_subset)
+ prefer 3
+ unfolding setge_def
+ apply (rule_tac x="- h x" in exI)
+ apply safe
+ apply (rule *)
+ using assms(3)[rule_format,OF x]
+ unfolding real_norm_def abs_le_iff
+ apply auto
+ done
show "((\<lambda>k. Inf {f j x |j. k \<le> j}) ---> g x) sequentially"
- proof (rule LIMSEQ_I) case goal1 hence "0<r/2" by auto
+ proof (rule LIMSEQ_I)
+ case goal1
+ hence "0<r/2" by auto
+ from assms(4)[THEN bspec, THEN LIMSEQ_D, OF x this] guess N .. note N = this
+ show ?case
+ apply (rule_tac x=N in exI,safe)
+ unfolding real_norm_def
+ apply (rule le_less_trans[of _ "r/2"])
+ apply (rule Inf_asclose)
+ apply safe
+ defer
+ apply (rule less_imp_le)
+ using N goal1
+ apply auto
+ done
+ qed
+ qed
+ note inc2 = conjunctD2[OF this]
+
+ have "g integrable_on s \<and>
+ ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) ---> integral s g) sequentially"
+ apply (rule monotone_convergence_decreasing,safe)
+ apply fact
+ proof -
+ show "bounded {integral s (\<lambda>x. Sup {f j x |j. k \<le> j}) |k. True}"
+ unfolding bounded_iff
+ apply (rule_tac x="integral s h" in exI)
+ proof safe
+ fix k :: nat
+ show "norm (integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) \<le> integral s h"
+ apply (rule integral_norm_bound_integral)
+ apply fact+
+ unfolding real_norm_def
+ apply rule
+ apply (rule Sup_abs_le)
+ using assms(3)
+ apply auto
+ done
+ qed
+ fix k :: nat and x
+ assume x: "x \<in> s"
+
+ show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}"
+ apply -
+ apply (rule real_ge_sup_subset)
+ prefer 3
+ unfolding setle_def
+ apply (rule_tac x="h x" in exI)
+ apply safe
+ using assms(3)[rule_format,OF x]
+ unfolding real_norm_def abs_le_iff
+ apply auto
+ done
+ show "((\<lambda>k. Sup {f j x |j. k \<le> j}) ---> g x) sequentially"
+ proof (rule LIMSEQ_I)
+ case goal1
+ hence "0<r/2" by auto
from assms(4)[THEN bspec, THEN LIMSEQ_D, OF x this] guess N .. note N=this
- show ?case apply(rule_tac x=N in exI,safe) unfolding real_norm_def
- apply(rule le_less_trans[of _ "r/2"]) apply(rule Inf_asclose) apply safe
- defer apply(rule less_imp_le) using N goal1 by auto
- qed qed note inc2 = conjunctD2[OF this]
-
- have "g integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) ---> integral s g) sequentially"
- apply(rule monotone_convergence_decreasing,safe) apply fact
- proof- show "bounded {integral s (\<lambda>x. Sup {f j x |j. k \<le> j}) |k. True}"
- unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
- proof safe fix k::nat
- show "norm (integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) \<le> integral s h"
- apply(rule integral_norm_bound_integral) apply fact+
- unfolding real_norm_def apply(rule) apply(rule Sup_abs_le) using assms(3) by auto
- qed fix k::nat and x assume x:"x\<in>s"
-
- show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}" apply-
- apply(rule real_ge_sup_subset) prefer 3 unfolding setle_def
- apply(rule_tac x="h x" in exI) apply safe
- using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
- show "((\<lambda>k. Sup {f j x |j. k \<le> j}) ---> g x) sequentially"
- proof (rule LIMSEQ_I) case goal1 hence "0<r/2" by auto
- from assms(4)[THEN bspec, THEN LIMSEQ_D, OF x this] guess N .. note N=this
- show ?case apply(rule_tac x=N in exI,safe) unfolding real_norm_def
- apply(rule le_less_trans[of _ "r/2"]) apply(rule Sup_asclose) apply safe
- defer apply(rule less_imp_le) using N goal1 by auto
- qed qed note dec2 = conjunctD2[OF this]
+ show ?case
+ apply (rule_tac x=N in exI,safe)
+ unfolding real_norm_def
+ apply (rule le_less_trans[of _ "r/2"])
+ apply (rule Sup_asclose)
+ apply safe
+ defer
+ apply (rule less_imp_le)
+ using N goal1
+ apply auto
+ done
+ qed
+ qed
+ note dec2 = conjunctD2[OF this]
show "g integrable_on s" by fact
show "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
- proof (rule LIMSEQ_I) case goal1
+ proof (rule LIMSEQ_I)
+ case goal1
from LIMSEQ_D [OF inc2(2) goal1] guess N1 .. note N1=this[unfolded real_norm_def]
from LIMSEQ_D [OF dec2(2) goal1] guess N2 .. note N2=this[unfolded real_norm_def]
- show ?case apply(rule_tac x="N1+N2" in exI,safe)
- proof- fix n assume n:"n \<ge> N1 + N2"
- have *:"\<And>i0 i i1 g. \<bar>i0 - g\<bar> < r \<longrightarrow> \<bar>i1 - g\<bar> < r \<longrightarrow> i0 \<le> i \<longrightarrow> i \<le> i1 \<longrightarrow> \<bar>i - g\<bar> < r" by arith
- show "norm (integral s (f n) - integral s g) < r" unfolding real_norm_def
- apply(rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
- proof- show "integral s (\<lambda>x. Inf {f j x |j. n \<le> j}) \<le> integral s (f n)"
- proof(rule integral_le[OF dec1(1) assms(1)],safe)
- fix x assume x:"x \<in> s" have *:"\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
- show "Inf {f j x |j. n \<le> j} \<le> f n x" apply(rule Inf_lower[where z="- h x"]) defer
- apply(rule *) using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
- qed show "integral s (f n) \<le> integral s (\<lambda>x. Sup {f j x |j. n \<le> j})"
- proof(rule integral_le[OF assms(1) inc1(1)],safe)
- fix x assume x:"x \<in> s"
- show "f n x \<le> Sup {f j x |j. n \<le> j}" apply(rule Sup_upper[where z="h x"]) defer
- using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
- qed qed(insert n,auto) qed qed qed
+ show ?case
+ apply (rule_tac x="N1+N2" in exI, safe)
+ proof -
+ fix n
+ assume n: "n \<ge> N1 + N2"
+ have *: "\<And>i0 i i1 g. \<bar>i0 - g\<bar> < r \<longrightarrow> \<bar>i1 - g\<bar> < r \<longrightarrow> i0 \<le> i \<longrightarrow> i \<le> i1 \<longrightarrow> \<bar>i - g\<bar> < r"
+ by arith
+ show "norm (integral s (f n) - integral s g) < r"
+ unfolding real_norm_def
+ apply (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
+ proof -
+ show "integral s (\<lambda>x. Inf {f j x |j. n \<le> j}) \<le> integral s (f n)"
+ proof (rule integral_le[OF dec1(1) assms(1)], safe)
+ fix x
+ assume x: "x \<in> s"
+ have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
+ show "Inf {f j x |j. n \<le> j} \<le> f n x"
+ apply (rule Inf_lower[where z="- h x"])
+ defer
+ apply (rule *)
+ using assms(3)[rule_format,OF x]
+ unfolding real_norm_def abs_le_iff
+ apply auto
+ done
+ qed
+ show "integral s (f n) \<le> integral s (\<lambda>x. Sup {f j x |j. n \<le> j})"
+ proof (rule integral_le[OF assms(1) inc1(1)], safe)
+ fix x
+ assume x: "x \<in> s"
+ show "f n x \<le> Sup {f j x |j. n \<le> j}"
+ apply (rule Sup_upper[where z="h x"])
+ defer
+ using assms(3)[rule_format,OF x]
+ unfolding real_norm_def abs_le_iff
+ apply auto
+ done
+ qed
+ qed (insert n, auto)
+ qed
+ qed
+qed
end
--- a/src/Pure/Concurrent/future.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/Concurrent/future.ML Wed Jan 16 22:18:46 2013 +0100
@@ -55,6 +55,8 @@
val interruptible_task: ('a -> 'b) -> 'a -> 'b
val cancel_group: group -> unit
val cancel: 'a future -> unit
+ val error_msg: Position.T -> (serial * string) * string option -> unit
+ val identify_result: Position.T -> 'a Exn.result -> 'a Exn.result
type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
val default_params: params
val forks: params -> (unit -> 'a) list -> 'a future list
@@ -433,14 +435,25 @@
fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
-(* future jobs *)
+(* results *)
+
+fun error_msg pos ((serial, msg), exec_id) =
+ Position.setmp_thread_data pos (fn () =>
+ if is_none exec_id orelse exec_id = Position.get_id pos
+ then Output.error_msg' (serial, msg) else warning msg) ();
-fun assign_result group result raw_res =
+fun identify_result pos res =
+ (case res of
+ Exn.Exn exn =>
+ let val exec_id =
+ (case Position.get_id pos of
+ NONE => []
+ | SOME id => [(Markup.exec_idN, id)])
+ in Exn.Exn (Par_Exn.identify exec_id exn) end
+ | _ => res);
+
+fun assign_result group result res =
let
- val res =
- (case raw_res of
- Exn.Exn exn => Exn.Exn (#2 (Par_Exn.serial exn))
- | _ => raw_res);
val _ = Single_Assignment.assign result res
handle exn as Fail _ =>
(case Single_Assignment.peek result of
@@ -453,6 +466,9 @@
| Exn.Res _ => true);
in ok end;
+
+(* future jobs *)
+
fun future_job group interrupts (e: unit -> 'a) =
let
val result = Single_Assignment.var "future" : 'a result;
@@ -467,7 +483,7 @@
then Multithreading.private_interrupts else Multithreading.no_interrupts)
(fn _ => Position.setmp_thread_data pos e ())) ()
else Exn.interrupt_exn;
- in assign_result group result res end;
+ in assign_result group result (identify_result pos res) end;
in (result, job) end;
@@ -563,7 +579,7 @@
val task = Task_Queue.dummy_task;
val group = Task_Queue.group_of_task task;
val result = Single_Assignment.var "value" : 'a result;
- val _ = assign_result group result res;
+ val _ = assign_result group result (identify_result (Position.thread_data ()) res);
in Future {promised = false, task = task, result = result} end;
fun value x = value_result (Exn.Res x);
@@ -619,7 +635,9 @@
else
let
val group = Task_Queue.group_of_task task;
- fun job ok = assign_result group result (if ok then res else Exn.interrupt_exn);
+ val pos = Position.thread_data ();
+ fun job ok =
+ assign_result group result (if ok then identify_result pos res else Exn.interrupt_exn);
val _ =
Multithreading.with_attributes Multithreading.no_interrupts (fn _ =>
let
--- a/src/Pure/Concurrent/par_exn.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/Concurrent/par_exn.ML Wed Jan 16 22:18:46 2013 +0100
@@ -7,7 +7,8 @@
signature PAR_EXN =
sig
- val serial: exn -> serial * exn
+ val identify: Properties.entry list -> exn -> exn
+ val the_serial: exn -> int
val make: exn list -> exn
val dest: exn -> exn list option
val is_interrupted: 'a Exn.result list -> bool
@@ -20,16 +21,17 @@
(* identification via serial numbers *)
-fun serial exn =
- (case get_exn_serial exn of
- SOME i => (i, exn)
- | NONE =>
- let
- val i = Library.serial ();
- val exn' = uninterruptible (fn _ => set_exn_serial i) exn;
- in (i, exn') end);
+fun identify default_props exn =
+ let
+ val props = Exn_Properties.get exn;
+ val update_serial =
+ if Properties.defined props Markup.serialN then []
+ else [(Markup.serialN, serial_string ())];
+ val update_props = filter_out (Properties.defined props o #1) default_props;
+ in Exn_Properties.update (update_serial @ update_props) exn end;
-val the_serial = the o get_exn_serial;
+fun the_serial exn =
+ Markup.parse_int (the (Properties.get (Exn_Properties.get exn) Markup.serialN));
val exn_ord = rev_order o int_ord o pairself the_serial;
@@ -41,7 +43,7 @@
no occurrences of Par_Exn or Exn.Interrupt*)
fun par_exns (Par_Exn exns) = exns
- | par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)];
+ | par_exns exn = if Exn.is_interrupt exn then [] else [identify [] exn];
fun make exns =
(case Ord_List.unions exn_ord (map par_exns exns) of
--- a/src/Pure/General/position.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/General/position.ML Wed Jan 16 22:18:46 2013 +0100
@@ -26,6 +26,7 @@
val id_only: string -> T
val get_id: T -> string option
val put_id: string -> T -> T
+ val parse_id: T -> int option
val of_properties: Properties.T -> T
val properties_of: T -> Properties.T
val def_properties_of: T -> Properties.T
@@ -123,6 +124,8 @@
fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
+fun parse_id pos = Option.map Markup.parse_int (get_id pos);
+
(* markup properties *)
--- a/src/Pure/Isar/proof.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/Isar/proof.ML Wed Jan 16 22:18:46 2013 +0100
@@ -827,7 +827,8 @@
val (finish_text, terminal_pos, finished_pos) =
(case opt_text of
NONE => (Method.finish_text (NONE, immed), Position.none, prev_pos)
- | SOME (text, (pos, end_pos)) => (Method.finish_text (SOME text, immed), pos, end_pos));
+ | SOME (text, (pos, end_pos)) =>
+ (Method.finish_text (SOME text, immed), Position.set_range (pos, end_pos), end_pos));
in
Seq.APPEND (fn state =>
state
--- a/src/Pure/Isar/runtime.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/Isar/runtime.ML Wed Jan 16 22:18:46 2013 +0100
@@ -12,6 +12,7 @@
exception TOPLEVEL_ERROR
val debug: bool Unsynchronized.ref
val exn_context: Proof.context option -> exn -> exn
+ val exn_messages_ids: (exn -> Position.T) -> exn -> ((serial * string) * string option) list
val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list
val exn_message: (exn -> Position.T) -> exn -> string
val debugging: ('a -> 'b) -> 'a -> 'b
@@ -42,10 +43,27 @@
(* exn_message *)
+local
+
fun if_context NONE _ _ = []
| if_context (SOME ctxt) f xs = map (f ctxt) xs;
-fun exn_messages exn_position e =
+fun identify exn =
+ let
+ val exn' = Par_Exn.identify [] exn;
+ val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN;
+ in ((Par_Exn.the_serial exn', exn'), exec_id) end;
+
+fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
+ | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
+ | flatten context exn =
+ (case Par_Exn.dest exn of
+ SOME exns => maps (flatten context) exns
+ | NONE => [(context, identify exn)]);
+
+in
+
+fun exn_messages_ids exn_position e =
let
fun raised exn name msgs =
let val pos = Position.here (exn_position exn) in
@@ -55,17 +73,10 @@
| _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
end;
- fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
- | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
- | flatten context exn =
- (case Par_Exn.dest exn of
- SOME exns => maps (flatten context) exns
- | NONE => [(context, Par_Exn.serial exn)]);
-
- fun exn_msgs (context, (i, exn)) =
+ fun exn_msgs (context, ((i, exn), id)) =
(case exn of
EXCURSION_FAIL (exn, loc) =>
- map (apsnd (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)))
+ map (fn ((i, msg), id) => ((i, msg ^ Markup.markup Markup.no_report ("\n" ^ loc)), id))
(sorted_msgs context exn)
| _ =>
let
@@ -90,12 +101,17 @@
raised exn ("THM " ^ string_of_int i)
(msg :: if_context context Display.string_of_thm thms)
| _ => raised exn (General.exnMessage exn) []);
- in [(i, msg)] end)
+ in [((i, msg), id)] end)
and sorted_msgs context exn =
- sort_distinct (int_ord o pairself fst) (maps exn_msgs (flatten context exn));
+ sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
in sorted_msgs NONE e end;
+end;
+
+fun exn_messages exn_position exn =
+ map #1 (exn_messages_ids exn_position exn);
+
fun exn_message exn_position exn =
(case exn_messages exn_position exn of
[] => "Interrupt"
--- a/src/Pure/Isar/toplevel.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML Wed Jan 16 22:18:46 2013 +0100
@@ -88,7 +88,6 @@
val unknown_context: transition -> transition
val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
val status: transition -> Markup.T -> unit
- val error_msg: transition -> serial * string -> unit
val add_hook: (transition -> state -> state -> unit) -> unit
val transition: bool -> transition -> state -> (state * (exn * string) option) option
val command: transition -> state -> state
@@ -596,9 +595,6 @@
fun status tr m =
setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
-fun error_msg tr msg =
- setmp_thread_position tr (fn () => Output.error_msg' msg) ();
-
(* post-transition hooks *)
--- a/src/Pure/ML-Systems/compiler_polyml.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ML-Systems/compiler_polyml.ML Wed Jan 16 22:18:46 2013 +0100
@@ -1,8 +1,6 @@
(* Title: Pure/ML-Systems/compiler_polyml.ML
-Runtime compilation for Poly/ML 5.3.0 or later.
-
-See also Pure/ML/ml_compiler_polyml.ML for advanced version.
+Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML).
*)
local
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Wed Jan 16 22:18:46 2013 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/ML-Systems/multithreading_polyml.ML
Author: Makarius
-Multithreading in Poly/ML 5.3.0 or later (cf. polyml/basis/Thread.sml).
+Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
*)
signature MULTITHREADING_POLYML =
--- a/src/Pure/ML-Systems/polyml.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ML-Systems/polyml.ML Wed Jan 16 22:18:46 2013 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/ML-Systems/polyml.ML
Author: Makarius
-Compatibility wrapper for Poly/ML 5.3.0 or later.
+Compatibility wrapper for Poly/ML.
*)
(* exceptions *)
@@ -11,22 +11,6 @@
NONE => raise exn
| SOME location => PolyML.raiseWithLocation (exn, location));
-fun set_exn_serial i exn =
- let
- val (file, startLine, endLine) =
- (case PolyML.exceptionLocation exn of
- NONE => ("", 0, 0)
- | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine));
- val location =
- {file = file, startLine = startLine, endLine = endLine,
- startPosition = ~ i, endPosition = 0};
- in PolyML.raiseWithLocation (exn, location) handle e => e end;
-
-fun get_exn_serial exn =
- (case Option.map #startPosition (PolyML.exceptionLocation exn) of
- NONE => NONE
- | SOME i => if i >= 0 then NONE else SOME (~ i));
-
exception Interrupt = SML90.Interrupt;
use "General/exn.ML";
--- a/src/Pure/ML-Systems/smlnj.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Wed Jan 16 22:18:46 2013 +0100
@@ -1,14 +1,12 @@
(* Title: Pure/ML-Systems/smlnj.ML
-Compatibility file for Standard ML of New Jersey 110 or later.
+Compatibility file for Standard ML of New Jersey.
*)
use "ML-Systems/proper_int.ML";
exception Interrupt;
fun reraise exn = raise exn;
-fun set_exn_serial (_: int) (exn: exn) = exn;
-fun get_exn_serial (exn: exn) : int option = NONE;
use "ML-Systems/overloading_smlnj.ML";
use "General/exn.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/exn_properties_dummy.ML Wed Jan 16 22:18:46 2013 +0100
@@ -0,0 +1,20 @@
+(* Title: Pure/ML/exn_properties_dummy.ML
+ Author: Makarius
+
+Exception properties -- dummy version.
+*)
+
+signature EXN_PROPERTIES =
+sig
+ val get: exn -> Properties.T
+ val update: Properties.entry list -> exn -> exn
+end;
+
+structure Exn_Properties: EXN_PROPERTIES =
+struct
+
+fun get _ = [];
+fun update _ exn = exn;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/exn_properties_polyml.ML Wed Jan 16 22:18:46 2013 +0100
@@ -0,0 +1,50 @@
+(* Title: Pure/ML/exn_properties_polyml.ML
+ Author: Makarius
+
+Exception properties for Poly/ML.
+*)
+
+signature EXN_PROPERTIES =
+sig
+ val of_location: PolyML.location -> Properties.T
+ val get: exn -> Properties.T
+ val update: Properties.entry list -> exn -> exn
+end;
+
+structure Exn_Properties: EXN_PROPERTIES =
+struct
+
+fun of_location (loc: PolyML.location) =
+ (case YXML.parse_body (#file loc) of
+ [] => []
+ | [XML.Text file] => [(Markup.fileN, file)]
+ | body => XML.Decode.properties body);
+
+fun get exn =
+ (case PolyML.exceptionLocation exn of
+ NONE => []
+ | SOME loc => of_location loc);
+
+fun update entries exn =
+ let
+ val loc =
+ the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
+ (PolyML.exceptionLocation exn);
+ val props = of_location loc;
+ val props' = fold Properties.put entries props;
+ in
+ if props = props' then exn
+ else
+ let
+ val loc' =
+ {file = YXML.string_of_body (XML.Encode.properties props'),
+ startLine = #startLine loc, endLine = #endLine loc,
+ startPosition = #startPosition loc, endPosition = #endPosition loc};
+ in
+ uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) ()
+ handle exn' => exn'
+ end
+ end;
+
+end;
+
--- a/src/Pure/ML/install_pp_polyml.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ML/install_pp_polyml.ML Wed Jan 16 22:18:46 2013 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/ML/install_pp_polyml.ML
Author: Makarius
-Extra toplevel pretty-printing for Poly/ML 5.3.0 or later.
+Extra toplevel pretty-printing for Poly/ML.
*)
PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
--- a/src/Pure/ML/ml_compiler.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ML/ml_compiler.ML Wed Jan 16 22:18:46 2013 +0100
@@ -7,6 +7,7 @@
signature ML_COMPILER =
sig
val exn_position: exn -> Position.T
+ val exn_messages_ids: exn -> ((serial * string) * string option) list
val exn_messages: exn -> (serial * string) list
val exn_message: exn -> string
val eval: bool -> Position.T -> ML_Lex.token list -> unit
@@ -16,6 +17,7 @@
struct
fun exn_position _ = Position.none;
+val exn_messages_ids = Runtime.exn_messages_ids exn_position;
val exn_messages = Runtime.exn_messages exn_position;
val exn_message = Runtime.exn_message exn_position;
--- a/src/Pure/ML/ml_compiler_polyml.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML Wed Jan 16 22:18:46 2013 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/ML/ml_compiler_polyml.ML
Author: Makarius
-Advanced runtime compilation for Poly/ML 5.3.0 or later.
+Advanced runtime compilation for Poly/ML.
*)
structure ML_Compiler: ML_COMPILER =
@@ -11,12 +11,8 @@
fun position_of (loc: PolyML.location) =
let
- val {file = text, startLine = line, startPosition = offset,
- endLine = _, endPosition = end_offset} = loc;
- val props =
- (case YXML.parse text of
- XML.Elem ((e, atts), _) => if e = Markup.positionN then atts else []
- | XML.Text s => Position.file_name s);
+ val {startLine = line, startPosition = offset, endPosition = end_offset, ...} = loc;
+ val props = Exn_Properties.of_location loc;
in
Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
end;
@@ -26,6 +22,7 @@
NONE => Position.none
| SOME loc => position_of loc);
+val exn_messages_ids = Runtime.exn_messages_ids exn_position;
val exn_messages = Runtime.exn_messages exn_position;
val exn_message = Runtime.exn_message exn_position;
@@ -71,10 +68,7 @@
(* input *)
- val location_props =
- op ^
- (YXML.output_markup (Markup.position |> Markup.properties
- (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))));
+ val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
val input_buffer =
Unsynchronized.ref (toks |> map
--- a/src/Pure/PIDE/command.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/PIDE/command.ML Wed Jan 16 22:18:46 2013 +0100
@@ -64,15 +64,15 @@
fun run int tr st =
(case Toplevel.transition int tr st of
SOME (st', NONE) => ([], SOME st')
- | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
- | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
+ | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE)
+ | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE));
fun check_cmts tr cmts st =
Toplevel.setmp_thread_position tr
(fn () => cmts
|> maps (fn cmt =>
(Thy_Output.check_text (Token.source_position_of cmt) st; [])
- handle exn => ML_Compiler.exn_messages exn)) ();
+ handle exn => ML_Compiler.exn_messages_ids exn)) ();
fun timing tr t =
if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
@@ -106,7 +106,7 @@
val errs = errs1 @ errs2;
val _ = timing tr (Timing.result start);
val _ = Toplevel.status tr Markup.finished;
- val _ = List.app (Toplevel.error_msg tr) errs;
+ val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
in
(case result of
NONE =>
--- a/src/Pure/PIDE/markup.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/PIDE/markup.ML Wed Jan 16 22:18:46 2013 +0100
@@ -107,6 +107,7 @@
val finishedN: string val finished: T
val failedN: string val failed: T
val serialN: string
+ val exec_idN: string
val initN: string
val statusN: string
val resultN: string
@@ -364,6 +365,7 @@
(* messages *)
val serialN = "serial";
+val exec_idN = "exec_id";
val initN = "init";
val statusN = "status";
--- a/src/Pure/ROOT Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ROOT Wed Jan 16 22:18:46 2013 +0100
@@ -139,6 +139,8 @@
"ML/ml_compiler_polyml.ML"
"ML/ml_context.ML"
"ML/ml_env.ML"
+ "ML/exn_properties_dummy.ML"
+ "ML/exn_properties_polyml.ML"
"ML/ml_lex.ML"
"ML/ml_parse.ML"
"ML/ml_statistics_dummy.ML"
--- a/src/Pure/ROOT.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/ROOT.ML Wed Jan 16 22:18:46 2013 +0100
@@ -70,6 +70,10 @@
(* concurrency within the ML runtime *)
+if ML_System.is_polyml
+then use "ML/exn_properties_polyml.ML"
+else use "ML/exn_properties_dummy.ML";
+
if ML_System.name = "polyml-5.5.0"
then use "ML/ml_statistics_polyml-5.5.0.ML"
else use "ML/ml_statistics_dummy.ML";
--- a/src/Pure/System/isabelle_process.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/System/isabelle_process.ML Wed Jan 16 22:18:46 2013 +0100
@@ -74,17 +74,16 @@
Synchronized.change command_tracing_messages (K Inttab.empty);
fun update_tracing () =
- (case Position.get_id (Position.thread_data ()) of
+ (case Position.parse_id (Position.thread_data ()) of
NONE => ()
| SOME id =>
let
- val i = Markup.parse_int id;
val (n, ok) =
Synchronized.change_result command_tracing_messages (fn tab =>
let
- val n = the_default 0 (Inttab.lookup tab i) + 1;
+ val n = the_default 0 (Inttab.lookup tab id) + 1;
val ok = n <= ! tracing_messages;
- in ((n, ok), Inttab.update (i, n) tab) end);
+ in ((n, ok), Inttab.update (id, n) tab) end);
in
if ok then ()
else
@@ -97,7 +96,7 @@
handle Fail _ => error "Stopped";
in
Synchronized.change command_tracing_messages
- (Inttab.map_default (i, 0) (fn k => k - m))
+ (Inttab.map_default (id, 0) (fn k => k - m))
end
end);
--- a/src/Pure/System/isar.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/System/isar.ML Wed Jan 16 22:18:46 2013 +0100
@@ -96,7 +96,8 @@
NONE => false
| SOME (_, SOME exn_info) =>
(set_exn (SOME exn_info);
- Toplevel.error_msg tr (serial (), ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
+ Toplevel.setmp_thread_position tr
+ Output.error_msg' (serial (), ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
true)
| SOME (st', NONE) =>
let
--- a/src/Pure/goal.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/goal.ML Wed Jan 16 22:18:46 2013 +0100
@@ -137,11 +137,10 @@
fun fork_name name e =
uninterruptible (fn _ => fn () =>
let
- val id =
- (case Position.get_id (Position.thread_data ()) of
- NONE => 0
- | SOME id => Markup.parse_int id);
+ val pos = Position.thread_data ();
+ val id = the_default 0 (Position.parse_id pos);
val _ = count_forked 1;
+
val future =
(singleton o Future.forks)
{name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
@@ -149,7 +148,9 @@
let
val task = the (Future.worker_task ());
val _ = status task [Markup.running];
- val result = Exn.capture (Future.interruptible_task e) ();
+ val result =
+ Exn.capture (Future.interruptible_task e) ()
+ |> Future.identify_result pos;
val _ = status task [Markup.finished, Markup.joined];
val _ =
(case result of
@@ -159,7 +160,7 @@
else
(status task [Markup.failed];
Output.report (Markup.markup_only Markup.bad);
- Output.error_msg (ML_Compiler.exn_message exn)));
+ List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn)));
val _ = count_forked ~1;
in Exn.release result end);
val _ = status (Future.task_of future) [Markup.forked];
--- a/src/Pure/library.ML Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Pure/library.ML Wed Jan 16 22:18:46 2013 +0100
@@ -204,8 +204,6 @@
exception RANDOM
val random: unit -> real
val random_range: int -> int -> int
- val one_of: 'a list -> 'a
- val frequency: (int * 'a) list -> 'a
(*misc*)
val divide_and_conquer: ('a -> 'a list * ('b list -> 'b)) -> 'a -> 'b
@@ -1021,15 +1019,6 @@
if h < l orelse l < 0 then raise RANDOM
else l + Real.floor (rmod (random ()) (real (h - l + 1)));
-fun one_of xs = nth xs (random_range 0 (length xs - 1));
-
-fun frequency xs =
- let
- val sum = foldl op + (0, map fst xs);
- fun pick n ((k: int, x) :: xs) =
- if n <= k then x else pick (n - k) xs
- in pick (random_range 1 sum) xs end;
-
(** misc **)
--- a/src/Tools/jEdit/src/document_view.scala Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Wed Jan 16 22:18:46 2013 +0100
@@ -70,7 +70,7 @@
def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value)
val rich_text_area =
- new Rich_Text_Area(text_area.getView, text_area, get_rendering _,
+ new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (),
caret_visible = true, hovering = false)
--- a/src/Tools/jEdit/src/pretty_text_area.scala Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Wed Jan 16 22:18:46 2013 +0100
@@ -55,6 +55,7 @@
class Pretty_Text_Area(
view: View,
background: Option[Color] = None,
+ close_action: () => Unit = () => (),
propagate_keys: Boolean = false) extends JEditEmbeddedTextArea
{
text_area =>
@@ -71,7 +72,7 @@
private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
private val rich_text_area =
- new Rich_Text_Area(view, text_area, () => current_rendering,
+ new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
caret_visible = false, hovering = true)
def refresh()
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Wed Jan 16 22:18:46 2013 +0100
@@ -55,7 +55,8 @@
/* pretty text area */
- val pretty_text_area = new Pretty_Text_Area(view, Some(rendering.tooltip_color), true)
+ val pretty_text_area =
+ new Pretty_Text_Area(view, Some(rendering.tooltip_color), () => window.dispose(), true)
pretty_text_area.resize(Rendering.font_family(),
Rendering.font_size("jedit_tooltip_font_scale").round)
pretty_text_area.update(rendering.snapshot, results, body)
--- a/src/Tools/jEdit/src/rich_text_area.scala Wed Jan 16 19:02:40 2013 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Wed Jan 16 22:18:46 2013 +0100
@@ -27,6 +27,7 @@
view: View,
text_area: TextArea,
get_rendering: () => Rendering,
+ close_action: () => Unit,
caret_visible: Boolean,
hovering: Boolean)
{
@@ -158,7 +159,9 @@
case None =>
}
active_area.text_info match {
- case Some((text, Text.Info(_, markup))) => Active.action(view, text, markup)
+ case Some((text, Text.Info(_, markup))) =>
+ Active.action(view, text, markup)
+ close_action()
case None =>
}
}