author wenzelm Wed, 16 Jan 2013 22:18:46 +0100 changeset 50920 1d5e1ac6693c parent 50908 02ed5abcc0e5 (current diff) parent 50919 cc03437a1f80 (diff) child 50921 287c79b9550c
merged
--- 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 @@

-(* 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 @@
(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 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
-      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 _ =
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.
-
+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 @@
Author:     Makarius

*)

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 "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.
*)

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 =
(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));
+        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 _ = status task [Markup.running];
-              val result = Exn.capture (Future.interruptible_task e) ();
+              val result =
+                |> Future.identify_result pos;
val _ = status task [Markup.finished, Markup.joined];
val _ =
(case result of
@@ -159,7 +160,7 @@
else
-                       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 =>
}
}