Merge
authorpaulson <lp15@cam.ac.uk>
Tue Mar 17 12:23:56 2015 +0000 (2015-03-17)
changeset 597317fccaeec22f0
parent 59730 b7c394c7a619
parent 59712 6c013328b885
child 59732 f13bb49dba08
Merge
NEWS
src/HOL/Codegenerator_Test/Candidates.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Transcendental.thy
     1.1 --- a/NEWS	Mon Mar 16 15:30:00 2015 +0000
     1.2 +++ b/NEWS	Tue Mar 17 12:23:56 2015 +0000
     1.3 @@ -178,6 +178,14 @@
     1.4      is invoked). The solution is to specify the case rule explicitly
     1.5      (e.g. "cases w rule: widget.exhaust").
     1.6      INCOMPATIBILITY.
     1.7 +  - Renamed theories:
     1.8 +      BNF_Comp ~> BNF_Composition
     1.9 +      BNF_FP_Base ~> BNF_Fixpoint_Base
    1.10 +      BNF_GFP ~> BNF_Greatest_Fixpoint
    1.11 +      BNF_LFP ~> BNF_Least_Fixpoint
    1.12 +      BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions
    1.13 +      Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions
    1.14 +    INCOMPATIBILITY.
    1.15  
    1.16  * Old datatype package:
    1.17    - The old 'datatype' command has been renamed 'old_datatype', and
     2.1 --- a/src/HOL/Bali/DeclConcepts.thy	Mon Mar 16 15:30:00 2015 +0000
     2.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Tue Mar 17 12:23:56 2015 +0000
     2.3 @@ -368,7 +368,7 @@
     2.4  class) to a qualified member declaration:  @{text method}  *}
     2.5  
     2.6  definition
     2.7 -  method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
     2.8 +  "method" :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
     2.9    where "method sig m = (declclass m, mdecl (sig, mthd m))"
    2.10  
    2.11  lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"
     3.1 --- a/src/HOL/Codegenerator_Test/Candidates.thy	Mon Mar 16 15:30:00 2015 +0000
     3.2 +++ b/src/HOL/Codegenerator_Test/Candidates.thy	Tue Mar 17 12:23:56 2015 +0000
     3.3 @@ -28,6 +28,13 @@
     3.4  
     3.5  code_pred sublist .
     3.6  
     3.7 +lemma [code]:  -- {* for the generic factorial function *}
     3.8 +  fixes XXX :: "'a :: semiring_numeral_div"
     3.9 +  shows
    3.10 +   "fact 0       = (1 :: 'a)"
    3.11 +   "fact (Suc n) = (of_nat (Suc n) * fact n :: 'a)"
    3.12 + by simp_all
    3.13 +
    3.14  code_reserved SML upto -- {* avoid popular infix *}
    3.15  
    3.16  end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Inequalities.thy	Tue Mar 17 12:23:56 2015 +0000
     4.3 @@ -0,0 +1,97 @@
     4.4 +(*  Title:     Inequalities
     4.5 +    Author:    Tobias Nipkow
     4.6 +    Author:    Johannes Hölzl
     4.7 +*)
     4.8 +
     4.9 +theory Inequalities
    4.10 +  imports Real_Vector_Spaces
    4.11 +begin
    4.12 +
    4.13 +lemma setsum_triangle_reindex:
    4.14 +  fixes n :: nat
    4.15 +  shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
    4.16 +  apply (simp add: setsum.Sigma)
    4.17 +  apply (rule setsum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
    4.18 +  apply auto
    4.19 +  done
    4.20 +
    4.21 +lemma gauss_sum_div2: "(2::'a::semiring_div) \<noteq> 0 \<Longrightarrow>
    4.22 +  setsum of_nat {1..n} = of_nat n * (of_nat n + 1) div (2::'a)"
    4.23 +using gauss_sum[where n=n and 'a = 'a,symmetric] by auto
    4.24 +
    4.25 +lemma Setsum_Icc_int: assumes "0 \<le> m" and "(m::int) \<le> n"
    4.26 +shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
    4.27 +proof-
    4.28 +  { fix k::int assume "k\<ge>0"
    4.29 +    hence "\<Sum> {1..k::int} = k * (k+1) div 2"
    4.30 +      by (rule gauss_sum_div2[where 'a = int, transferred]) simp
    4.31 +  } note 1 = this
    4.32 +  have "{m..n} = {0..n} - {0..m-1}" using `m\<ge>0` by auto
    4.33 +  hence "\<Sum>{m..n} = \<Sum>{0..n} - \<Sum>{0..m-1}" using assms
    4.34 +    by (force intro!: setsum_diff)
    4.35 +  also have "{0..n} = {0} Un {1..n}" using assms by auto
    4.36 +  also have "\<Sum>({0} \<union> {1..n}) = \<Sum>{1..n}" by(simp add: setsum.union_disjoint)
    4.37 +  also have "\<dots> = n * (n+1) div 2" by(rule 1[OF order_trans[OF assms]])
    4.38 +  also have "{0..m-1} = (if m=0 then {} else {0} Un {1..m-1})"
    4.39 +    using assms by auto
    4.40 +  also have "\<Sum> \<dots> = m*(m-1) div 2" using `m\<ge>0` by(simp add: 1 mult.commute)
    4.41 +  also have "n*(n+1) div 2 - m*(m-1) div 2 = (n*(n+1) - m*(m-1)) div 2"
    4.42 +    apply(subgoal_tac "even(n*(n+1)) \<and> even(m*(m-1))")
    4.43 +    by (auto (*simp: even_def[symmetric]*))
    4.44 +  finally show ?thesis .
    4.45 +qed
    4.46 +
    4.47 +lemma Setsum_Icc_nat: assumes "(m::nat) \<le> n"
    4.48 +shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
    4.49 +proof -
    4.50 +  have "m*(m-1) \<le> n*(n + 1)"
    4.51 +   using assms by (meson diff_le_self order_trans le_add1 mult_le_mono)
    4.52 +  hence "int(\<Sum> {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms
    4.53 +    by (auto simp add: Setsum_Icc_int[transferred, OF _ assms] zdiv_int int_mult
    4.54 +      split: zdiff_int_split)
    4.55 +  thus ?thesis by simp
    4.56 +qed
    4.57 +
    4.58 +lemma Setsum_Ico_nat: assumes "(m::nat) \<le> n"
    4.59 +shows "\<Sum> {m..<n} = (n*(n-1) - m*(m-1)) div 2"
    4.60 +proof cases
    4.61 +  assume "m < n"
    4.62 +  hence "{m..<n} = {m..n-1}" by auto
    4.63 +  hence "\<Sum>{m..<n} = \<Sum>{m..n-1}" by simp
    4.64 +  also have "\<dots> = (n*(n-1) - m*(m-1)) div 2"
    4.65 +    using assms `m < n` by (simp add: Setsum_Icc_nat mult.commute)
    4.66 +  finally show ?thesis .
    4.67 +next
    4.68 +  assume "\<not> m < n" with assms show ?thesis by simp
    4.69 +qed
    4.70 +
    4.71 +lemma Chebyshev_sum_upper:
    4.72 +  fixes a b::"nat \<Rightarrow> 'a::linordered_idom"
    4.73 +  assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> a i \<le> a j"
    4.74 +  assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> b i \<ge> b j"
    4.75 +  shows "of_nat n * (\<Sum>k=0..<n. a k * b k) \<le> (\<Sum>k=0..<n. a k) * (\<Sum>k=0..<n. b k)"
    4.76 +proof -
    4.77 +  let ?S = "(\<Sum>j=0..<n. (\<Sum>k=0..<n. (a j - a k) * (b j - b k)))"
    4.78 +  have "2 * (of_nat n * (\<Sum>j=0..<n. (a j * b j)) - (\<Sum>j=0..<n. b j) * (\<Sum>k=0..<n. a k)) = ?S"
    4.79 +    unfolding one_add_one[symmetric] algebra_simps
    4.80 +    by (simp add: algebra_simps setsum_subtractf setsum.distrib setsum.commute[of "\<lambda>i j. a i * b j"] setsum_right_distrib)
    4.81 +  also
    4.82 +  { fix i j::nat assume "i<n" "j<n"
    4.83 +    hence "a i - a j \<le> 0 \<and> b i - b j \<ge> 0 \<or> a i - a j \<ge> 0 \<and> b i - b j \<le> 0"
    4.84 +      using assms by (cases "i \<le> j") (auto simp: algebra_simps)
    4.85 +  } hence "?S \<le> 0"
    4.86 +    by (auto intro!: setsum_nonpos simp: mult_le_0_iff)
    4.87 +       (auto simp: field_simps)
    4.88 +  finally show ?thesis by (simp add: algebra_simps)
    4.89 +qed
    4.90 +
    4.91 +lemma Chebyshev_sum_upper_nat:
    4.92 +  fixes a b :: "nat \<Rightarrow> nat"
    4.93 +  shows "(\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> a i \<le> a j) \<Longrightarrow>
    4.94 +         (\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> b i \<ge> b j) \<Longrightarrow>
    4.95 +    n * (\<Sum>i=0..<n. a i * b i) \<le> (\<Sum>i=0..<n. a i) * (\<Sum>i=0..<n. b i)"
    4.96 +using Chebyshev_sum_upper[where 'a=real, of n a b]
    4.97 +by (simp del: real_of_nat_mult real_of_nat_setsum
    4.98 +  add: real_of_nat_mult[symmetric] real_of_nat_setsum[symmetric] real_of_nat_def[symmetric])
    4.99 +
   4.100 +end
     5.1 --- a/src/HOL/Library/Extended_Real.thy	Mon Mar 16 15:30:00 2015 +0000
     5.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Mar 17 12:23:56 2015 +0000
     5.3 @@ -2602,6 +2602,50 @@
     5.4    (is "?lhs \<longleftrightarrow> ?rhs")
     5.5    unfolding le_Liminf_iff eventually_sequentially ..
     5.6  
     5.7 +lemma Liminf_add_le:
     5.8 +  fixes f g :: "_ \<Rightarrow> ereal"
     5.9 +  assumes F: "F \<noteq> bot"
    5.10 +  assumes ev: "eventually (\<lambda>x. 0 \<le> f x) F" "eventually (\<lambda>x. 0 \<le> g x) F"
    5.11 +  shows "Liminf F f + Liminf F g \<le> Liminf F (\<lambda>x. f x + g x)"
    5.12 +  unfolding Liminf_def
    5.13 +proof (subst SUP_ereal_add_left[symmetric])
    5.14 +  let ?F = "{P. eventually P F}"
    5.15 +  let ?INF = "\<lambda>P g. INFIMUM (Collect P) g"
    5.16 +  show "?F \<noteq> {}"
    5.17 +    by (auto intro: eventually_True)
    5.18 +  show "(SUP P:?F. ?INF P g) \<noteq> - \<infinity>"
    5.19 +    unfolding bot_ereal_def[symmetric] SUP_bot_conv INF_eq_bot_iff
    5.20 +    by (auto intro!: exI[of _ 0] ev simp: bot_ereal_def)
    5.21 +  have "(SUP P:?F. ?INF P f + (SUP P:?F. ?INF P g)) \<le> (SUP P:?F. (SUP P':?F. ?INF P f + ?INF P' g))"
    5.22 +  proof (safe intro!: SUP_mono bexI[of _ "\<lambda>x. P x \<and> 0 \<le> f x" for P])
    5.23 +    fix P let ?P' = "\<lambda>x. P x \<and> 0 \<le> f x"
    5.24 +    assume "eventually P F"
    5.25 +    with ev show "eventually ?P' F"
    5.26 +      by eventually_elim auto
    5.27 +    have "?INF P f + (SUP P:?F. ?INF P g) \<le> ?INF ?P' f + (SUP P:?F. ?INF P g)"
    5.28 +      by (intro ereal_add_mono INF_mono) auto
    5.29 +    also have "\<dots> = (SUP P':?F. ?INF ?P' f + ?INF P' g)"
    5.30 +    proof (rule SUP_ereal_add_right[symmetric])
    5.31 +      show "INFIMUM {x. P x \<and> 0 \<le> f x} f \<noteq> - \<infinity>"
    5.32 +        unfolding bot_ereal_def[symmetric] INF_eq_bot_iff
    5.33 +        by (auto intro!: exI[of _ 0] ev simp: bot_ereal_def)
    5.34 +    qed fact
    5.35 +    finally show "?INF P f + (SUP P:?F. ?INF P g) \<le> (SUP P':?F. ?INF ?P' f + ?INF P' g)" .
    5.36 +  qed
    5.37 +  also have "\<dots> \<le> (SUP P:?F. INF x:Collect P. f x + g x)"
    5.38 +  proof (safe intro!: SUP_least)
    5.39 +    fix P Q assume *: "eventually P F" "eventually Q F"
    5.40 +    show "?INF P f + ?INF Q g \<le> (SUP P:?F. INF x:Collect P. f x + g x)"
    5.41 +    proof (rule SUP_upper2)
    5.42 +      show "(\<lambda>x. P x \<and> Q x) \<in> ?F"
    5.43 +        using * by (auto simp: eventually_conj)
    5.44 +      show "?INF P f + ?INF Q g \<le> (INF x:{x. P x \<and> Q x}. f x + g x)"
    5.45 +        by (intro INF_greatest ereal_add_mono) (auto intro: INF_lower)
    5.46 +    qed
    5.47 +  qed
    5.48 +  finally show "(SUP P:?F. ?INF P f + (SUP P:?F. ?INF P g)) \<le> (SUP P:?F. INF x:Collect P. f x + g x)" .
    5.49 +qed
    5.50 +
    5.51  
    5.52  subsubsection {* Tests for code generator *}
    5.53  
     6.1 --- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Mon Mar 16 15:30:00 2015 +0000
     6.2 +++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Tue Mar 17 12:23:56 2015 +0000
     6.3 @@ -429,14 +429,14 @@
     6.4    fixes G ("\<Gamma>") and Phi ("\<Phi>")
     6.5    assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"  
     6.6    assumes is_class: "is_class \<Gamma> C"
     6.7 -    and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
     6.8 +    and "method": "method (\<Gamma>,C) (m,[]) = Some (C, b)"
     6.9      and m: "m \<noteq> init"
    6.10    defines start: "s \<equiv> start_state \<Gamma> C m"
    6.11  
    6.12    assumes s: "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> t" 
    6.13    shows "t \<noteq> TypeError"
    6.14  proof -
    6.15 -  from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
    6.16 +  from wt is_class "method" have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
    6.17      unfolding start by (rule BV_correct_initial)
    6.18    from wt this s show ?thesis by (rule no_type_errors)
    6.19  qed
    6.20 @@ -461,12 +461,12 @@
    6.21    fixes G ("\<Gamma>") and Phi ("\<Phi>")
    6.22    assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"  
    6.23    assumes is_class: "is_class \<Gamma> C"
    6.24 -    and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
    6.25 +    and "method": "method (\<Gamma>,C) (m,[]) = Some (C, b)"
    6.26      and m: "m \<noteq> init"
    6.27    defines start: "s \<equiv> start_state \<Gamma> C m"
    6.28    shows "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s \<midarrow>jvm\<rightarrow> t"
    6.29  proof -
    6.30 -  from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
    6.31 +  from wt is_class "method" have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
    6.32      unfolding start by (rule BV_correct_initial)
    6.33    with wt show ?thesis by (rule welltyped_commutes)
    6.34  qed
     7.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Mon Mar 16 15:30:00 2015 +0000
     7.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Mar 17 12:23:56 2015 +0000
     7.3 @@ -811,7 +811,7 @@
     7.4  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
     7.5  proof -
     7.6    assume wtprog: "wt_jvm_prog G phi"
     7.7 -  assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
     7.8 +  assume "method": "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
     7.9    assume ins:    "ins ! pc = Invoke C' mn pTs"
    7.10    assume wti:    "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
    7.11    assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
    7.12 @@ -823,7 +823,7 @@
    7.13      wfprog: "wf_prog wfmb G" 
    7.14      by (simp add: wt_jvm_prog_def)
    7.15        
    7.16 -  from ins method approx
    7.17 +  from ins "method" approx
    7.18    obtain s where
    7.19      heap_ok: "G\<turnstile>h hp\<surd>" and
    7.20      prealloc:"preallocated hp" and
    7.21 @@ -880,7 +880,7 @@
    7.22    from stk' l_o l
    7.23    have oX_pos: "last (take (Suc (length pTs)) stk) = oX" by simp
    7.24  
    7.25 -  with state' method ins no_xcp oX_conf
    7.26 +  with state' "method" ins no_xcp oX_conf
    7.27    obtain ref where oX_Addr: "oX = Addr ref"
    7.28      by (auto simp add: raise_system_xcpt_def dest: conf_RefTD)
    7.29  
    7.30 @@ -922,7 +922,7 @@
    7.31        
    7.32    from loc obj_ty have "fst (the (hp ref)) = D" by (simp add: obj_ty_def)
    7.33  
    7.34 -  with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD no_xcp
    7.35 +  with oX_Addr oX_pos state' "method" ins stk' l_o l loc obj_ty mD no_xcp
    7.36    have state'_val:
    7.37      "state' =
    7.38       Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' undefined, 
    7.39 @@ -972,7 +972,7 @@
    7.40      show ?thesis by (simp add: correct_frame_def)
    7.41    qed
    7.42  
    7.43 -  from state'_val heap_ok mD'' ins method phi_pc s X' l mX
    7.44 +  from state'_val heap_ok mD'' ins "method" phi_pc s X' l mX
    7.45         frames s' LT0 c_f is_class_C stk' oX_Addr frame prealloc and l
    7.46    show ?thesis
    7.47      apply (simp add: correct_state_def)
     8.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Mon Mar 16 15:30:00 2015 +0000
     8.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Mar 17 12:23:56 2015 +0000
     8.3 @@ -177,7 +177,7 @@
     8.4  qed
     8.5  
     8.6  consts
     8.7 -  method :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
     8.8 +  "method" :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
     8.9    field  :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty     )" (* ###curry *)
    8.10    fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
    8.11  
     9.1 --- a/src/HOL/NSA/Examples/NSPrimes.thy	Mon Mar 16 15:30:00 2015 +0000
     9.2 +++ b/src/HOL/NSA/Examples/NSPrimes.thy	Tue Mar 17 12:23:56 2015 +0000
     9.3 @@ -13,8 +13,6 @@
     9.4  text{*These can be used to derive an alternative proof of the infinitude of
     9.5  primes by considering a property of nonstandard sets.*}
     9.6  
     9.7 -declare dvd_def [transfer_refold]
     9.8 -
     9.9  definition
    9.10    starprime :: "hypnat set" where
    9.11    [transfer_unfold]: "starprime = ( *s* {p. prime p})"
    10.1 --- a/src/HOL/NSA/StarDef.thy	Mon Mar 16 15:30:00 2015 +0000
    10.2 +++ b/src/HOL/NSA/StarDef.thy	Tue Mar 17 12:23:56 2015 +0000
    10.3 @@ -848,6 +848,14 @@
    10.4  instance star :: (semiring_1) semiring_1 ..
    10.5  instance star :: (comm_semiring_1) comm_semiring_1 ..
    10.6  
    10.7 +declare dvd_def [transfer_refold]
    10.8 +
    10.9 +instance star :: (semiring_dvd) semiring_dvd
   10.10 +apply intro_classes
   10.11 +apply(transfer, rule dvd_add_times_triv_left_iff)
   10.12 +apply(transfer, erule (1) dvd_addD)
   10.13 +done
   10.14 +
   10.15  instance star :: (no_zero_divisors) no_zero_divisors
   10.16  by (intro_classes, transfer, rule no_zero_divisors)
   10.17  
   10.18 @@ -857,6 +865,16 @@
   10.19  instance star :: (comm_ring) comm_ring ..
   10.20  instance star :: (ring_1) ring_1 ..
   10.21  instance star :: (comm_ring_1) comm_ring_1 ..
   10.22 +instance star :: (semiring_no_zero_divisors) semiring_no_zero_divisors ..
   10.23 +instance star :: (semiring_div) semiring_div
   10.24 +apply intro_classes
   10.25 +apply(transfer, rule mod_div_equality)
   10.26 +apply(transfer, rule div_by_0)
   10.27 +apply(transfer, rule div_0)
   10.28 +apply(transfer, erule div_mult_self1)
   10.29 +apply(transfer, erule div_mult_mult1)
   10.30 +done
   10.31 +
   10.32  instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
   10.33  instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
   10.34  instance star :: (idom) idom .. 
   10.35 @@ -924,7 +942,6 @@
   10.36  instance star :: (linordered_field) linordered_field ..
   10.37  instance star :: (linordered_field_inverse_zero) linordered_field_inverse_zero ..
   10.38  
   10.39 -
   10.40  subsection {* Power *}
   10.41  
   10.42  lemma star_power_def [transfer_unfold]:
   10.43 @@ -1006,6 +1023,36 @@
   10.44  
   10.45  instance star :: (ring_char_0) ring_char_0 ..
   10.46  
   10.47 +instance star :: (semiring_parity) semiring_parity
   10.48 +apply intro_classes
   10.49 +apply(transfer, rule odd_one)
   10.50 +apply(transfer, erule (1) odd_even_add)
   10.51 +apply(transfer, erule even_multD)
   10.52 +apply(transfer, erule odd_ex_decrement)
   10.53 +done
   10.54 +
   10.55 +instance star :: (semiring_div_parity) semiring_div_parity
   10.56 +apply intro_classes
   10.57 +apply(transfer, rule parity)
   10.58 +apply(transfer, rule one_mod_two_eq_one)
   10.59 +apply(transfer, rule zero_not_eq_two)
   10.60 +done
   10.61 +
   10.62 +instance star :: (semiring_numeral_div) semiring_numeral_div
   10.63 +apply intro_classes
   10.64 +apply(transfer, erule semiring_numeral_div_class.diff_invert_add1)
   10.65 +apply(transfer, erule semiring_numeral_div_class.le_add_diff_inverse2)
   10.66 +apply(transfer, rule semiring_numeral_div_class.mult_div_cancel)
   10.67 +apply(transfer, erule (1) semiring_numeral_div_class.div_less)
   10.68 +apply(transfer, erule (1) semiring_numeral_div_class.mod_less)
   10.69 +apply(transfer, erule (1) semiring_numeral_div_class.div_positive)
   10.70 +apply(transfer, erule semiring_numeral_div_class.mod_less_eq_dividend)
   10.71 +apply(transfer, erule semiring_numeral_div_class.pos_mod_bound)
   10.72 +apply(transfer, erule semiring_numeral_div_class.pos_mod_sign)
   10.73 +apply(transfer, erule semiring_numeral_div_class.mod_mult2_eq)
   10.74 +apply(transfer, erule semiring_numeral_div_class.div_mult2_eq)
   10.75 +apply(transfer, rule discrete)
   10.76 +done
   10.77  
   10.78  subsection {* Finite class *}
   10.79  
    11.1 --- a/src/HOL/NanoJava/TypeRel.thy	Mon Mar 16 15:30:00 2015 +0000
    11.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Tue Mar 17 12:23:56 2015 +0000
    11.3 @@ -108,7 +108,7 @@
    11.4  done
    11.5  
    11.6  --{* Methods of a class, with inheritance and hiding *}
    11.7 -definition method :: "cname => (mname \<rightharpoonup> methd)" where
    11.8 +definition "method" :: "cname => (mname \<rightharpoonup> methd)" where
    11.9    "method C \<equiv> class_rec C methods"
   11.10  
   11.11  lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
    12.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Mar 16 15:30:00 2015 +0000
    12.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Mar 17 12:23:56 2015 +0000
    12.3 @@ -793,6 +793,9 @@
    12.4  
    12.5  subsection \<open> Conditional Probabilities \<close>
    12.6  
    12.7 +lemma measure_pmf_zero_iff: "measure (measure_pmf p) s = 0 \<longleftrightarrow> set_pmf p \<inter> s = {}"
    12.8 +  by (subst measure_pmf.prob_eq_0) (auto simp: AE_measure_pmf_iff)
    12.9 +
   12.10  context
   12.11    fixes p :: "'a pmf" and s :: "'a set"
   12.12    assumes not_empty: "set_pmf p \<inter> s \<noteq> {}"
   12.13 @@ -854,32 +857,22 @@
   12.14  qed
   12.15  
   12.16  lemma bind_cond_pmf_cancel:
   12.17 -  assumes in_S: "\<And>x. x \<in> set_pmf p \<Longrightarrow> x \<in> S x" "\<And>x. x \<in> set_pmf q \<Longrightarrow> x \<in> S x"
   12.18 -  assumes S_eq: "\<And>x y. x \<in> S y \<Longrightarrow> S x = S y"
   12.19 -  and same: "\<And>x. measure (measure_pmf p) (S x) = measure (measure_pmf q) (S x)"
   12.20 -  shows "bind_pmf p (\<lambda>x. cond_pmf q (S x)) = q" (is "?lhs = _")
   12.21 +  assumes [simp]: "\<And>x. x \<in> set_pmf p \<Longrightarrow> set_pmf q \<inter> {y. R x y} \<noteq> {}"
   12.22 +  assumes [simp]: "\<And>y. y \<in> set_pmf q \<Longrightarrow> set_pmf p \<inter> {x. R x y} \<noteq> {}"
   12.23 +  assumes [simp]: "\<And>x y. x \<in> set_pmf p \<Longrightarrow> y \<in> set_pmf q \<Longrightarrow> R x y \<Longrightarrow> measure q {y. R x y} = measure p {x. R x y}"
   12.24 +  shows "bind_pmf p (\<lambda>x. cond_pmf q {y. R x y}) = q"
   12.25  proof (rule pmf_eqI)
   12.26 -  { fix x
   12.27 -    assume "x \<in> set_pmf p"
   12.28 -    hence "set_pmf p \<inter> (S x) \<noteq> {}" using in_S by auto
   12.29 -    hence "measure (measure_pmf p) (S x) \<noteq> 0"
   12.30 -      by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff)
   12.31 -    with same have "measure (measure_pmf q) (S x) \<noteq> 0" by simp
   12.32 -    hence "set_pmf q \<inter> S x \<noteq> {}"
   12.33 -      by(auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) }
   12.34 -  note [simp] = this
   12.35 -
   12.36 -  fix z
   12.37 -  have pmf_q_z: "z \<notin> S z \<Longrightarrow> pmf q z = 0"
   12.38 -    by(erule contrapos_np)(simp add: pmf_eq_0_set_pmf in_S)
   12.39 -
   12.40 -  have "ereal (pmf ?lhs z) = \<integral>\<^sup>+ x. ereal (pmf (cond_pmf q (S x)) z) \<partial>measure_pmf p"
   12.41 -    by(simp add: ereal_pmf_bind)
   12.42 -  also have "\<dots> = \<integral>\<^sup>+ x. ereal (pmf q z / measure p (S z)) * indicator (S z) x \<partial>measure_pmf p"
   12.43 -    by(rule nn_integral_cong_AE)(auto simp add: AE_measure_pmf_iff pmf_cond same pmf_q_z in_S dest!: S_eq split: split_indicator)
   12.44 -  also have "\<dots> = pmf q z" using pmf_nonneg[of q z]
   12.45 -    by (subst nn_integral_cmult)(auto simp add: measure_nonneg measure_pmf.emeasure_eq_measure same measure_pmf.prob_eq_0 AE_measure_pmf_iff pmf_eq_0_set_pmf in_S)
   12.46 -  finally show "pmf ?lhs z = pmf q z" by simp
   12.47 +  fix i
   12.48 +  have "ereal (pmf (bind_pmf p (\<lambda>x. cond_pmf q {y. R x y})) i) =
   12.49 +    (\<integral>\<^sup>+x. ereal (pmf q i / measure p {x. R x i}) * ereal (indicator {x. R x i} x) \<partial>p)"
   12.50 +    by (auto simp add: ereal_pmf_bind AE_measure_pmf_iff pmf_cond pmf_eq_0_set_pmf intro!: nn_integral_cong_AE)
   12.51 +  also have "\<dots> = (pmf q i * measure p {x. R x i}) / measure p {x. R x i}"
   12.52 +    by (simp add: pmf_nonneg measure_nonneg zero_ereal_def[symmetric] ereal_indicator
   12.53 +                  nn_integral_cmult measure_pmf.emeasure_eq_measure)
   12.54 +  also have "\<dots> = pmf q i"
   12.55 +    by (cases "pmf q i = 0") (simp_all add: pmf_eq_0_set_pmf measure_measure_pmf_not_zero)
   12.56 +  finally show "pmf (bind_pmf p (\<lambda>x. cond_pmf q {y. R x y})) i = pmf q i"
   12.57 +    by simp
   12.58  qed
   12.59  
   12.60  subsection \<open> Relator \<close>
   12.61 @@ -891,6 +884,136 @@
   12.62       map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk>
   12.63    \<Longrightarrow> rel_pmf R p q"
   12.64  
   12.65 +lemma rel_pmfI:
   12.66 +  assumes R: "rel_set R (set_pmf p) (set_pmf q)"
   12.67 +  assumes eq: "\<And>x y. x \<in> set_pmf p \<Longrightarrow> y \<in> set_pmf q \<Longrightarrow> R x y \<Longrightarrow>
   12.68 +    measure p {x. R x y} = measure q {y. R x y}"
   12.69 +  shows "rel_pmf R p q"
   12.70 +proof
   12.71 +  let ?pq = "bind_pmf p (\<lambda>x. bind_pmf (cond_pmf q {y. R x y}) (\<lambda>y. return_pmf (x, y)))"
   12.72 +  have "\<And>x. x \<in> set_pmf p \<Longrightarrow> set_pmf q \<inter> {y. R x y} \<noteq> {}"
   12.73 +    using R by (auto simp: rel_set_def)
   12.74 +  then show "\<And>x y. (x, y) \<in> set_pmf ?pq \<Longrightarrow> R x y"
   12.75 +    by auto
   12.76 +  show "map_pmf fst ?pq = p"
   12.77 +    by (simp add: map_bind_pmf map_return_pmf bind_return_pmf')
   12.78 +
   12.79 +  show "map_pmf snd ?pq = q"
   12.80 +    using R eq
   12.81 +    apply (simp add: bind_cond_pmf_cancel map_bind_pmf map_return_pmf bind_return_pmf')
   12.82 +    apply (rule bind_cond_pmf_cancel)
   12.83 +    apply (auto simp: rel_set_def)
   12.84 +    done
   12.85 +qed
   12.86 +
   12.87 +lemma rel_pmf_imp_rel_set: "rel_pmf R p q \<Longrightarrow> rel_set R (set_pmf p) (set_pmf q)"
   12.88 +  by (force simp add: rel_pmf.simps rel_set_def)
   12.89 +
   12.90 +lemma rel_pmfD_measure:
   12.91 +  assumes rel_R: "rel_pmf R p q" and R: "\<And>a b. R a b \<Longrightarrow> R a y \<longleftrightarrow> R x b"
   12.92 +  assumes "x \<in> set_pmf p" "y \<in> set_pmf q"
   12.93 +  shows "measure p {x. R x y} = measure q {y. R x y}"
   12.94 +proof -
   12.95 +  from rel_R obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
   12.96 +    and eq: "p = map_pmf fst pq" "q = map_pmf snd pq"
   12.97 +    by (auto elim: rel_pmf.cases)
   12.98 +  have "measure p {x. R x y} = measure pq {x. R (fst x) y}"
   12.99 +    by (simp add: eq map_pmf_rep_eq measure_distr)
  12.100 +  also have "\<dots> = measure pq {y. R x (snd y)}"
  12.101 +    by (intro measure_pmf.finite_measure_eq_AE)
  12.102 +       (auto simp: AE_measure_pmf_iff R dest!: pq)
  12.103 +  also have "\<dots> = measure q {y. R x y}"
  12.104 +    by (simp add: eq map_pmf_rep_eq measure_distr)
  12.105 +  finally show "measure p {x. R x y} = measure q {y. R x y}" .
  12.106 +qed
  12.107 +
  12.108 +lemma rel_pmf_iff_measure:
  12.109 +  assumes "symp R" "transp R"
  12.110 +  shows "rel_pmf R p q \<longleftrightarrow>
  12.111 +    rel_set R (set_pmf p) (set_pmf q) \<and>
  12.112 +    (\<forall>x\<in>set_pmf p. \<forall>y\<in>set_pmf q. R x y \<longrightarrow> measure p {x. R x y} = measure q {y. R x y})"
  12.113 +  by (safe intro!: rel_pmf_imp_rel_set rel_pmfI)
  12.114 +     (auto intro!: rel_pmfD_measure dest: sympD[OF \<open>symp R\<close>] transpD[OF \<open>transp R\<close>])
  12.115 +
  12.116 +lemma quotient_rel_set_disjoint:
  12.117 +  "equivp R \<Longrightarrow> C \<in> UNIV // {(x, y). R x y} \<Longrightarrow> rel_set R A B \<Longrightarrow> A \<inter> C = {} \<longleftrightarrow> B \<inter> C = {}"
  12.118 +  using in_quotient_imp_closed[of UNIV "{(x, y). R x y}" C] 
  12.119 +  by (auto 0 0 simp: equivp_equiv rel_set_def set_eq_iff elim: equivpE)
  12.120 +     (blast dest: equivp_symp)+
  12.121 +
  12.122 +lemma quotientD: "equiv X R \<Longrightarrow> A \<in> X // R \<Longrightarrow> x \<in> A \<Longrightarrow> A = R `` {x}"
  12.123 +  by (metis Image_singleton_iff equiv_class_eq_iff quotientE)
  12.124 +
  12.125 +lemma rel_pmf_iff_equivp:
  12.126 +  assumes "equivp R"
  12.127 +  shows "rel_pmf R p q \<longleftrightarrow> (\<forall>C\<in>UNIV // {(x, y). R x y}. measure p C = measure q C)"
  12.128 +    (is "_ \<longleftrightarrow>   (\<forall>C\<in>_//?R. _)")
  12.129 +proof (subst rel_pmf_iff_measure, safe)
  12.130 +  show "symp R" "transp R"
  12.131 +    using assms by (auto simp: equivp_reflp_symp_transp)
  12.132 +next
  12.133 +  fix C assume C: "C \<in> UNIV // ?R" and R: "rel_set R (set_pmf p) (set_pmf q)"
  12.134 +  assume eq: "\<forall>x\<in>set_pmf p. \<forall>y\<in>set_pmf q. R x y \<longrightarrow> measure p {x. R x y} = measure q {y. R x y}"
  12.135 +  
  12.136 +  show "measure p C = measure q C"
  12.137 +  proof cases
  12.138 +    assume "p \<inter> C = {}"
  12.139 +    moreover then have "q \<inter> C = {}"  
  12.140 +      using quotient_rel_set_disjoint[OF assms C R] by simp
  12.141 +    ultimately show ?thesis
  12.142 +      unfolding measure_pmf_zero_iff[symmetric] by simp
  12.143 +  next
  12.144 +    assume "p \<inter> C \<noteq> {}"
  12.145 +    moreover then have "q \<inter> C \<noteq> {}"  
  12.146 +      using quotient_rel_set_disjoint[OF assms C R] by simp
  12.147 +    ultimately obtain x y where in_set: "x \<in> set_pmf p" "y \<in> set_pmf q" and in_C: "x \<in> C" "y \<in> C"
  12.148 +      by auto
  12.149 +    then have "R x y"
  12.150 +      using in_quotient_imp_in_rel[of UNIV ?R C x y] C assms
  12.151 +      by (simp add: equivp_equiv)
  12.152 +    with in_set eq have "measure p {x. R x y} = measure q {y. R x y}"
  12.153 +      by auto
  12.154 +    moreover have "{y. R x y} = C"
  12.155 +      using assms `x \<in> C` C quotientD[of UNIV ?R C x] by (simp add: equivp_equiv)
  12.156 +    moreover have "{x. R x y} = C"
  12.157 +      using assms `y \<in> C` C quotientD[of UNIV "?R" C y] sympD[of R]
  12.158 +      by (auto simp add: equivp_equiv elim: equivpE)
  12.159 +    ultimately show ?thesis
  12.160 +      by auto
  12.161 +  qed
  12.162 +next
  12.163 +  assume eq: "\<forall>C\<in>UNIV // ?R. measure p C = measure q C"
  12.164 +  show "rel_set R (set_pmf p) (set_pmf q)"
  12.165 +    unfolding rel_set_def
  12.166 +  proof safe
  12.167 +    fix x assume x: "x \<in> set_pmf p"
  12.168 +    have "{y. R x y} \<in> UNIV // ?R"
  12.169 +      by (auto simp: quotient_def)
  12.170 +    with eq have *: "measure q {y. R x y} = measure p {y. R x y}"
  12.171 +      by auto
  12.172 +    have "measure q {y. R x y} \<noteq> 0"
  12.173 +      using x assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp)
  12.174 +    then show "\<exists>y\<in>set_pmf q. R x y"
  12.175 +      unfolding measure_pmf_zero_iff by auto
  12.176 +  next
  12.177 +    fix y assume y: "y \<in> set_pmf q"
  12.178 +    have "{x. R x y} \<in> UNIV // ?R"
  12.179 +      using assms by (auto simp: quotient_def dest: equivp_symp)
  12.180 +    with eq have *: "measure p {x. R x y} = measure q {x. R x y}"
  12.181 +      by auto
  12.182 +    have "measure p {x. R x y} \<noteq> 0"
  12.183 +      using y assms unfolding * by (auto simp: measure_pmf_zero_iff set_eq_iff dest: equivp_reflp)
  12.184 +    then show "\<exists>x\<in>set_pmf p. R x y"
  12.185 +      unfolding measure_pmf_zero_iff by auto
  12.186 +  qed
  12.187 +
  12.188 +  fix x y assume "x \<in> set_pmf p" "y \<in> set_pmf q" "R x y"
  12.189 +  have "{y. R x y} \<in> UNIV // ?R" "{x. R x y} = {y. R x y}"
  12.190 +    using assms `R x y` by (auto simp: quotient_def dest: equivp_symp equivp_transp)
  12.191 +  with eq show "measure p {x. R x y} = measure q {y. R x y}"
  12.192 +    by auto
  12.193 +qed
  12.194 +
  12.195  bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf
  12.196  proof -
  12.197    show "map_pmf id = id" by (rule map_pmf_id)
  12.198 @@ -919,7 +1042,7 @@
  12.199        and x: "x \<in> set_pmf p"
  12.200      thus "f x = g x" by simp }
  12.201  
  12.202 -  fix R :: "'a => 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
  12.203 +  fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
  12.204    { fix p q r
  12.205      assume pq: "rel_pmf R p q"
  12.206        and qr:"rel_pmf S q r"
  12.207 @@ -928,8 +1051,8 @@
  12.208      from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z"
  12.209        and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto
  12.210  
  12.211 -    def pr \<equiv> "bind_pmf pq (\<lambda>(x, y). bind_pmf (cond_pmf qr {(y', z). y' = y}) (\<lambda>(y', z). return_pmf (x, z)))"
  12.212 -    have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {(y', z). y' = y} \<noteq> {}"
  12.213 +    def pr \<equiv> "bind_pmf pq (\<lambda>xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy}) (\<lambda>yz. return_pmf (fst xy, snd yz)))"
  12.214 +    have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {yz. fst yz = y} \<noteq> {}"
  12.215        by (force simp: q')
  12.216  
  12.217      have "rel_pmf (R OO S) p r"
  12.218 @@ -940,11 +1063,11 @@
  12.219        with pq qr show "(R OO S) x z"
  12.220          by blast
  12.221      next
  12.222 -      have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {(y', z). y' = y}))"
  12.223 -        by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_return_pmf)
  12.224 +      have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {yz. fst yz = y}))"
  12.225 +        by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_return_pmf map_pmf_comp)
  12.226        then show "map_pmf snd pr = r"
  12.227 -        unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) auto
  12.228 -    qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf map_pmf_def[symmetric] p) }
  12.229 +        unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) (auto simp: eq_commute)
  12.230 +    qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf map_pmf_def[symmetric] p map_pmf_comp) }
  12.231    then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
  12.232      by(auto simp add: le_fun_def)
  12.233  qed (fact natLeq_card_order natLeq_cinfinite)+
  12.234 @@ -1137,46 +1260,31 @@
  12.235    assumes 2: "rel_pmf R q p"
  12.236    and refl: "reflp R" and trans: "transp R"
  12.237    shows "rel_pmf (inf R R\<inverse>\<inverse>) p q"
  12.238 -proof
  12.239 -  let ?E = "\<lambda>x. {y. R x y \<and> R y x}"
  12.240 -  let ?\<mu>E = "\<lambda>x. measure q (?E x)"
  12.241 -  { fix x
  12.242 -    have "measure p (?E x) = measure p ({y. R x y} - {y. R x y \<and> \<not> R y x})"
  12.243 -      by(auto intro!: arg_cong[where f="measure p"])
  12.244 -    also have "\<dots> = measure p {y. R x y} - measure p {y. R x y \<and> \<not> R y x}"
  12.245 -      by (rule measure_pmf.finite_measure_Diff) auto
  12.246 -    also have "measure p {y. R x y \<and> \<not> R y x} = measure q {y. R x y \<and> \<not> R y x}"
  12.247 -      using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ioi)
  12.248 -    also have "measure p {y. R x y} = measure q {y. R x y}"
  12.249 -      using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ici)
  12.250 -    also have "measure q {y. R x y} - measure q {y. R x y \<and> ~ R y x} =
  12.251 -      measure q ({y. R x y} - {y. R x y \<and> \<not> R y x})"
  12.252 -      by(rule measure_pmf.finite_measure_Diff[symmetric]) auto
  12.253 -    also have "\<dots> = ?\<mu>E x"
  12.254 -      by(auto intro!: arg_cong[where f="measure q"])
  12.255 -    also note calculation }
  12.256 -  note eq = this
  12.257 +proof (subst rel_pmf_iff_equivp, safe)
  12.258 +  show "equivp (inf R R\<inverse>\<inverse>)"
  12.259 +    using trans refl by (auto simp: equivp_reflp_symp_transp intro: sympI transpI reflpI dest: transpD reflpD)
  12.260 +  
  12.261 +  fix C assume "C \<in> UNIV // {(x, y). inf R R\<inverse>\<inverse> x y}"
  12.262 +  then obtain x where C: "C = {y. R x y \<and> R y x}"
  12.263 +    by (auto elim: quotientE)
  12.264  
  12.265 -  def pq \<equiv> "bind_pmf p (\<lambda>x. bind_pmf (cond_pmf q (?E x)) (\<lambda>y. return_pmf (x, y)))"
  12.266 -
  12.267 -  show "map_pmf fst pq = p"
  12.268 -    by(simp add: pq_def map_bind_pmf map_return_pmf bind_return_pmf')
  12.269 -
  12.270 -  show "map_pmf snd pq = q"
  12.271 -    unfolding pq_def map_bind_pmf map_return_pmf bind_return_pmf' snd_conv
  12.272 -    by(subst bind_cond_pmf_cancel)(auto simp add: reflpD[OF \<open>reflp R\<close>] eq  intro: transpD[OF \<open>transp R\<close>])
  12.273 -
  12.274 -  fix x y
  12.275 -  assume "(x, y) \<in> set_pmf pq"
  12.276 -  moreover
  12.277 -  { assume "x \<in> set_pmf p"
  12.278 -    hence "measure (measure_pmf p) (?E x) \<noteq> 0"
  12.279 -      by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff intro: reflpD[OF \<open>reflp R\<close>])
  12.280 -    hence "measure (measure_pmf q) (?E x) \<noteq> 0" using eq by simp
  12.281 -    hence "set_pmf q \<inter> {y. R x y \<and> R y x} \<noteq> {}"
  12.282 -      by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) }
  12.283 -  ultimately show "inf R R\<inverse>\<inverse> x y"
  12.284 -    by (auto simp add: pq_def)
  12.285 +  let ?R = "\<lambda>x y. R x y \<and> R y x"
  12.286 +  let ?\<mu>R = "\<lambda>y. measure q {x. ?R x y}"
  12.287 +  have "measure p {y. ?R x y} = measure p ({y. R x y} - {y. R x y \<and> \<not> R y x})"
  12.288 +    by(auto intro!: arg_cong[where f="measure p"])
  12.289 +  also have "\<dots> = measure p {y. R x y} - measure p {y. R x y \<and> \<not> R y x}"
  12.290 +    by (rule measure_pmf.finite_measure_Diff) auto
  12.291 +  also have "measure p {y. R x y \<and> \<not> R y x} = measure q {y. R x y \<and> \<not> R y x}"
  12.292 +    using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ioi)
  12.293 +  also have "measure p {y. R x y} = measure q {y. R x y}"
  12.294 +    using 1 2 refl trans by(auto intro!: Orderings.antisym measure_Ici)
  12.295 +  also have "measure q {y. R x y} - measure q {y. R x y \<and> \<not> R y x} =
  12.296 +    measure q ({y. R x y} - {y. R x y \<and> \<not> R y x})"
  12.297 +    by(rule measure_pmf.finite_measure_Diff[symmetric]) auto
  12.298 +  also have "\<dots> = ?\<mu>R x"
  12.299 +    by(auto intro!: arg_cong[where f="measure q"])
  12.300 +  finally show "measure p C = measure q C"
  12.301 +    by (simp add: C conj_commute)
  12.302  qed
  12.303  
  12.304  lemma rel_pmf_antisym:
    13.1 --- a/src/HOL/Series.thy	Mon Mar 16 15:30:00 2015 +0000
    13.2 +++ b/src/HOL/Series.thy	Tue Mar 17 12:23:56 2015 +0000
    13.3 @@ -10,8 +10,8 @@
    13.4  section {* Infinite Series *}
    13.5  
    13.6  theory Series
    13.7 -imports Limits
    13.8 -begin
    13.9 +imports Limits Inequalities
   13.10 +begin 
   13.11  
   13.12  subsection {* Definition of infinite summability *}
   13.13  
   13.14 @@ -576,14 +576,6 @@
   13.15    @{url "http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm"}
   13.16  *}
   13.17  
   13.18 -lemma setsum_triangle_reindex:
   13.19 -  fixes n :: nat
   13.20 -  shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
   13.21 -  apply (simp add: setsum.Sigma)
   13.22 -  apply (rule setsum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
   13.23 -  apply auto
   13.24 -  done
   13.25 -
   13.26  lemma Cauchy_product_sums:
   13.27    fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
   13.28    assumes a: "summable (\<lambda>k. norm (a k))"
    14.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Mar 16 15:30:00 2015 +0000
    14.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 17 12:23:56 2015 +0000
    14.3 @@ -2424,7 +2424,7 @@
    14.4               forall is_some ctrs')
    14.5            end
    14.6        in
    14.7 -        ctrss |> map datatype_of_ctrs |> filter_out (null o #2)
    14.8 +        ctrss |> map datatype_of_ctrs |> filter #3
    14.9        end
   14.10      else
   14.11        []
    15.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 16 15:30:00 2015 +0000
    15.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Tue Mar 17 12:23:56 2015 +0000
    15.3 @@ -8,6 +8,8 @@
    15.4  
    15.5  signature BNF_COMP =
    15.6  sig
    15.7 +  val bnf_inline_threshold: int Config.T
    15.8 +
    15.9    val ID_bnf: BNF_Def.bnf
   15.10    val DEADID_bnf: BNF_Def.bnf
   15.11  
   15.12 @@ -54,6 +56,8 @@
   15.13  open BNF_Tactics
   15.14  open BNF_Comp_Tactics
   15.15  
   15.16 +val bnf_inline_threshold = Attrib.setup_config_int @{binding bnf_inline_threshold} (K 5);
   15.17 +
   15.18  val ID_bnf = the (bnf_of @{context} "BNF_Composition.ID");
   15.19  val DEADID_bnf = the (bnf_of @{context} "BNF_Composition.DEADID");
   15.20  
   15.21 @@ -730,12 +734,12 @@
   15.22  val mk_abs = mk_abs_or_rep range_type;
   15.23  val mk_rep = mk_abs_or_rep domain_type;
   15.24  
   15.25 -val smart_max_inline_type_size = 5; (*FUDGE*)
   15.26 -
   15.27 -fun maybe_typedef force_out_of_line (b, As, mx) set opt_morphs tac =
   15.28 +fun maybe_typedef ctxt force_out_of_line (b, As, mx) set opt_morphs tac =
   15.29    let
   15.30 +    val threshold = Config.get ctxt bnf_inline_threshold;
   15.31      val repT = HOLogic.dest_setT (fastype_of set);
   15.32 -    val out_of_line = force_out_of_line orelse Term.size_of_typ repT > smart_max_inline_type_size;
   15.33 +    val out_of_line = force_out_of_line orelse
   15.34 +      (threshold >= 0 andalso Term.size_of_typ repT > threshold);
   15.35    in
   15.36      if out_of_line then
   15.37        typedef (b, As, mx) set opt_morphs tac
   15.38 @@ -769,7 +773,7 @@
   15.39      val T_bind = qualify b;
   15.40      val TA_params = Term.add_tfreesT repTA (if has_live_phantoms then As' else []);
   15.41      val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) =
   15.42 -      maybe_typedef has_live_phantoms (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE
   15.43 +      maybe_typedef lthy has_live_phantoms (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE
   15.44          (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
   15.45  
   15.46      val repTB = mk_T_of_bnf Ds Bs bnf;
   15.47 @@ -799,7 +803,7 @@
   15.48      val all_deads = map TFree (fold Term.add_tfreesT Ds []);
   15.49  
   15.50      val ((bdT, (_, Abs_bd_name, _, _, Abs_bdT_inject, Abs_bdT_cases)), lthy) =
   15.51 -      maybe_typedef false (bdT_bind, params, NoSyn)
   15.52 +      maybe_typedef lthy false (bdT_bind, params, NoSyn)
   15.53          (HOLogic.mk_UNIV bd_repT) NONE (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
   15.54  
   15.55      val (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) =
    16.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Mar 16 15:30:00 2015 +0000
    16.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Mar 17 12:23:56 2015 +0000
    16.3 @@ -189,12 +189,6 @@
    16.4        map (cterm_instantiate_pos (map SOME (passives @ actives))) ctor_rec_transfers;
    16.5      val total_n = Integer.sum ns;
    16.6      val True = @{term True};
    16.7 -    fun magic eq xs xs' = Subgoal.FOCUS (fn {prems, ...} =>
    16.8 -      let
    16.9 -        val thm = prems
   16.10 -          |> Ctr_Sugar_Util.permute_like eq xs xs'
   16.11 -          |> Library.foldl1 (fn (acc, elem) => elem RS (acc RS @{thm rel_funD}))
   16.12 -      in HEADGOAL (rtac thm) end)
   16.13    in
   16.14      HEADGOAL Goal.conjunction_tac THEN
   16.15      EVERY (map (fn ctor_rec_transfer =>
    17.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 16 15:30:00 2015 +0000
    17.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Mar 17 12:23:56 2015 +0000
    17.3 @@ -155,6 +155,7 @@
    17.4  
    17.5    val mk_Inl: typ -> term -> term
    17.6    val mk_Inr: typ -> term -> term
    17.7 +  val mk_sumprod_balanced: typ -> int -> int -> term list -> term
    17.8    val mk_absumprod: typ -> term -> int -> int -> term list -> term
    17.9  
   17.10    val dest_sumT: typ -> typ * typ
   17.11 @@ -414,9 +415,11 @@
   17.12  
   17.13  val mk_tuple_balanced = mk_tuple1_balanced [];
   17.14  
   17.15 +fun mk_sumprod_balanced T n k ts = Sum_Tree.mk_inj T n k (mk_tuple_balanced ts);
   17.16 +
   17.17  fun mk_absumprod absT abs0 n k ts =
   17.18    let val abs = mk_abs absT abs0;
   17.19 -  in abs $ Sum_Tree.mk_inj (domain_type (fastype_of abs)) n k (mk_tuple_balanced ts) end;
   17.20 +  in abs $ mk_sumprod_balanced (domain_type (fastype_of abs)) n k ts end;
   17.21  
   17.22  fun mk_case_sum (f, g) =
   17.23    let
    18.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Mar 16 15:30:00 2015 +0000
    18.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 17 12:23:56 2015 +0000
    18.3 @@ -44,6 +44,21 @@
    18.4       fp_nesting_map_comps: thm list,
    18.5       ctr_specs: corec_ctr_spec list}
    18.6  
    18.7 +  val fold_rev_let_if_case: Proof.context -> (term list -> term -> 'a -> 'a) -> typ list ->
    18.8 +    term -> 'a -> 'a
    18.9 +  val massage_let_if_case: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
   18.10 +    typ list -> term -> term
   18.11 +  val massage_nested_corec_call: Proof.context -> (term -> bool) ->
   18.12 +    (typ list -> typ -> typ -> term -> term) -> typ list -> typ -> term -> term
   18.13 +  val expand_to_ctr_term: Proof.context -> string -> typ list -> term -> term
   18.14 +  val massage_corec_code_rhs: Proof.context -> (typ list -> term -> term list -> term) ->
   18.15 +    typ list -> term -> term
   18.16 +  val fold_rev_corec_code_rhs: Proof.context -> (term list -> term -> term list -> 'a -> 'a) ->
   18.17 +    typ list -> term -> 'a -> 'a
   18.18 +  val case_thms_of_term: Proof.context -> term ->
   18.19 +    thm list * thm list * thm list * thm list * thm list
   18.20 +  val map_thms_of_type: Proof.context -> typ -> thm list
   18.21 +
   18.22    val corec_specs_of: binding list -> typ list -> typ list -> term list ->
   18.23      (term * term list list) list list -> local_theory ->
   18.24      corec_spec list * typ list * thm * thm * thm list * thm list * (Token.src list * Token.src list)
   18.25 @@ -160,7 +175,6 @@
   18.26  val s_not_conj = conjuncts_s o s_not o mk_conjs;
   18.27  
   18.28  fun propagate_unit_pos u cs = if member (op aconv) cs u then [@{const False}] else cs;
   18.29 -
   18.30  fun propagate_unit_neg not_u cs = remove (op aconv) not_u cs;
   18.31  
   18.32  fun propagate_units css =
   18.33 @@ -421,9 +435,9 @@
   18.34        end)
   18.35    | _ => not_codatatype ctxt res_T);
   18.36  
   18.37 -fun map_thms_of_typ ctxt (Type (s, _)) =
   18.38 +fun map_thms_of_type ctxt (Type (s, _)) =
   18.39      (case fp_sugar_of ctxt s of SOME {fp_bnf_sugar = {map_thms, ...}, ...} => map_thms | NONE => [])
   18.40 -  | map_thms_of_typ _ _ = [];
   18.41 +  | map_thms_of_type _ _ = [];
   18.42  
   18.43  structure GFP_Rec_Sugar_Plugin = Plugin(type T = fp_rec_sugar);
   18.44  
   18.45 @@ -533,7 +547,7 @@
   18.46          co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
   18.47        {T = T, corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec,
   18.48         exhaust_discs = exhaust_discs, sel_defs = sel_defs,
   18.49 -       fp_nesting_maps = maps (map_thms_of_typ lthy o T_of_bnf) fp_nesting_bnfs,
   18.50 +       fp_nesting_maps = maps (map_thms_of_type lthy o T_of_bnf) fp_nesting_bnfs,
   18.51         fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs,
   18.52         fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs,
   18.53         ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms corec_discs
   18.54 @@ -931,7 +945,7 @@
   18.55          (build_corec_arg_nested_call ctxt has_call sel_eqns sel)) nested_calls'
   18.56      end);
   18.57  
   18.58 -fun build_codefs ctxt bs mxs has_call arg_Tss (corec_specs : corec_spec list)
   18.59 +fun build_defs ctxt bs mxs has_call arg_Tss (corec_specs : corec_spec list)
   18.60      (disc_eqnss : coeqn_data_disc list list) (sel_eqnss : coeqn_data_sel list list) =
   18.61    let
   18.62      val corecs = map #corec corec_specs;
   18.63 @@ -1104,7 +1118,7 @@
   18.64      val disc_eqnss = @{map 6} mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss
   18.65        disc_eqnss0;
   18.66      val (defs, excludess') =
   18.67 -      build_codefs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
   18.68 +      build_defs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
   18.69  
   18.70      val tac_opts =
   18.71        map (fn {code_rhs_opt, ...} :: _ =>
    19.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Mar 16 15:30:00 2015 +0000
    19.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Mar 17 12:23:56 2015 +0000
    19.3 @@ -539,14 +539,13 @@
    19.4  
    19.5      val defs = build_defs lthy nonexhaustives bs mxs funs_data rec_specs has_call;
    19.6  
    19.7 -    fun prove def_thms' ({ctr_specs, fp_nesting_map_ident0s, fp_nesting_map_comps, ...}
    19.8 -        : rec_spec) (fun_data : eqn_data list) lthy' =
    19.9 +    fun prove def_thms ({ctr_specs, fp_nesting_map_ident0s, fp_nesting_map_comps, ...} : rec_spec)
   19.10 +        (fun_data : eqn_data list) lthy' =
   19.11        let
   19.12          val js =
   19.13            find_indices (op = o apply2 (fn {fun_name, ctr, ...} => (fun_name, ctr)))
   19.14              fun_data eqns_data;
   19.15  
   19.16 -        val def_thms = map (snd o snd) def_thms';
   19.17          val simp_thms = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs
   19.18            |> fst
   19.19            |> map_filter (try (fn (x, [y]) =>
   19.20 @@ -587,7 +586,7 @@
   19.21               fun_defs = Morphism.fact phi def_thms, fpTs = take actual_nn Ts};
   19.22          in
   19.23            map_prod split_list (interpret_lfp_rec_sugar plugins fp_rec_sugar)
   19.24 -            (@{fold_map 2} (prove defs) (take actual_nn rec_specs) funs_data lthy)
   19.25 +            (@{fold_map 2} (prove (map (snd o snd) defs)) (take actual_nn rec_specs) funs_data lthy)
   19.26          end),
   19.27        lthy |> Local_Theory.notes (notes @ common_notes) |> snd)
   19.28    end;
    20.1 --- a/src/HOL/Transcendental.thy	Mon Mar 16 15:30:00 2015 +0000
    20.2 +++ b/src/HOL/Transcendental.thy	Tue Mar 17 12:23:56 2015 +0000
    20.3 @@ -16,6 +16,9 @@
    20.4  lemma real_fact_nat [simp]: "real (fact n :: nat) = fact n"
    20.5    by (simp add: real_of_nat_def)
    20.6  
    20.7 +lemma real_fact_int [simp]: "real (fact n :: int) = fact n"
    20.8 +  by (metis of_int_of_nat_eq of_nat_fact real_of_int_def)
    20.9 +
   20.10  lemma root_test_convergence:
   20.11    fixes f :: "nat \<Rightarrow> 'a::banach"
   20.12    assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup"
   20.13 @@ -4372,7 +4375,6 @@
   20.14          case False
   20.15          hence "0 < \<bar>x\<bar>" and "- \<bar>x\<bar> < \<bar>x\<bar>" by auto
   20.16          have "suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>) = suminf (?c 0) - arctan 0"
   20.17 -        thm suminf_eq_arctan_bounded
   20.18            by (rule suminf_eq_arctan_bounded[where x1="0" and a1="-\<bar>x\<bar>" and b1="\<bar>x\<bar>", symmetric])
   20.19              (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
   20.20          moreover
    21.1 --- a/src/Pure/GUI/gui.scala	Mon Mar 16 15:30:00 2015 +0000
    21.2 +++ b/src/Pure/GUI/gui.scala	Tue Mar 17 12:23:56 2015 +0000
    21.3 @@ -80,9 +80,10 @@
    21.4  
    21.5    /* simple dialogs */
    21.6  
    21.7 -  def scrollable_text(txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
    21.8 +  def scrollable_text(raw_txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
    21.9      : ScrollPane =
   21.10    {
   21.11 +    val txt = Output.clean_yxml(raw_txt)
   21.12      val text = new TextArea(txt)
   21.13      if (width > 0) text.columns = width
   21.14      if (height > 0 && split_lines(txt).length > height) text.rows = height
    22.1 --- a/src/Pure/General/exn.scala	Mon Mar 16 15:30:00 2015 +0000
    22.2 +++ b/src/Pure/General/exn.scala	Tue Mar 17 12:23:56 2015 +0000
    22.3 @@ -13,6 +13,13 @@
    22.4    /* exceptions as values */
    22.5  
    22.6    sealed abstract class Result[A]
    22.7 +  {
    22.8 +    def user_error: Result[A] =
    22.9 +      this match {
   22.10 +        case Exn(ERROR(msg)) => Exn(ERROR(msg))
   22.11 +        case _ => this
   22.12 +      }
   22.13 +  }
   22.14    case class Res[A](res: A) extends Result[A]
   22.15    case class Exn[A](exn: Throwable) extends Result[A]
   22.16  
   22.17 @@ -79,17 +86,18 @@
   22.18  
   22.19    /* message */
   22.20  
   22.21 -  private val runtime_exception = Class.forName("java.lang.RuntimeException")
   22.22 -
   22.23    def user_message(exn: Throwable): Option[String] =
   22.24 -    if (exn.isInstanceOf[java.io.IOException]) {
   22.25 -      val msg = exn.getMessage
   22.26 -      Some(if (msg == null) "I/O error" else "I/O error: " + msg)
   22.27 -    }
   22.28 -    else if (exn.getClass == runtime_exception) {
   22.29 +    if (exn.getClass == classOf[RuntimeException] ||
   22.30 +        exn.getClass == classOf[Library.User_Error])
   22.31 +    {
   22.32        val msg = exn.getMessage
   22.33        Some(if (msg == null || msg == "") "Error" else msg)
   22.34      }
   22.35 +    else if (exn.isInstanceOf[java.io.IOException])
   22.36 +    {
   22.37 +      val msg = exn.getMessage
   22.38 +      Some(if (msg == null || msg == "") "I/O error" else "I/O error: " + msg)
   22.39 +    }
   22.40      else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
   22.41      else None
   22.42  
    23.1 --- a/src/Pure/General/output.scala	Mon Mar 16 15:30:00 2015 +0000
    23.2 +++ b/src/Pure/General/output.scala	Tue Mar 17 12:23:56 2015 +0000
    23.3 @@ -10,11 +10,15 @@
    23.4  
    23.5  object Output
    23.6  {
    23.7 -  def warning_text(msg: String): String = cat_lines(split_lines(msg).map("### " + _))
    23.8 -  def error_text(msg: String): String = cat_lines(split_lines(msg).map("*** " + _))
    23.9 +  def clean_yxml(msg: String): String =
   23.10 +    try { XML.content(YXML.parse_body(msg)) }
   23.11 +    catch { case ERROR(_) => msg }
   23.12  
   23.13 -  def writeln(msg: String) { Console.err.println(msg) }
   23.14 +  def writeln_text(msg: String): String = clean_yxml(msg)
   23.15 +  def warning_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
   23.16 +  def error_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
   23.17 +
   23.18 +  def writeln(msg: String) { Console.err.println(writeln_text(msg)) }
   23.19    def warning(msg: String) { Console.err.println(warning_text(msg)) }
   23.20    def error_message(msg: String) { Console.err.println(error_text(msg)) }
   23.21  }
   23.22 -
    24.1 --- a/src/Pure/General/position.scala	Mon Mar 16 15:30:00 2015 +0000
    24.2 +++ b/src/Pure/General/position.scala	Tue Mar 17 12:23:56 2015 +0000
    24.3 @@ -21,6 +21,7 @@
    24.4    val End_Offset = new Properties.Int(Markup.END_OFFSET)
    24.5    val File = new Properties.String(Markup.FILE)
    24.6    val Id = new Properties.Long(Markup.ID)
    24.7 +  val Id_String = new Properties.String(Markup.ID)
    24.8  
    24.9    val Def_Line = new Properties.Int(Markup.DEF_LINE)
   24.10    val Def_Offset = new Properties.Int(Markup.DEF_OFFSET)
   24.11 @@ -102,18 +103,20 @@
   24.12    /* here: user output */
   24.13  
   24.14    def here(pos: T): String =
   24.15 -    (Line.unapply(pos), File.unapply(pos)) match {
   24.16 -      case (Some(i), None) => " (line " + i.toString + ")"
   24.17 -      case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
   24.18 -      case (None, Some(name)) => " (file " + quote(name) + ")"
   24.19 -      case _ => ""
   24.20 -    }
   24.21 +    Markup(Markup.POSITION, pos).markup(
   24.22 +      (Line.unapply(pos), File.unapply(pos)) match {
   24.23 +        case (Some(i), None) => " (line " + i.toString + ")"
   24.24 +        case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
   24.25 +        case (None, Some(name)) => " (file " + quote(name) + ")"
   24.26 +        case _ => ""
   24.27 +      })
   24.28  
   24.29    def here_undelimited(pos: T): String =
   24.30 -    (Line.unapply(pos), File.unapply(pos)) match {
   24.31 -      case (Some(i), None) => "line " + i.toString
   24.32 -      case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
   24.33 -      case (None, Some(name)) => "file " + quote(name)
   24.34 -      case _ => ""
   24.35 -    }
   24.36 +    Markup(Markup.POSITION, pos).markup(
   24.37 +      (Line.unapply(pos), File.unapply(pos)) match {
   24.38 +        case (Some(i), None) => "line " + i.toString
   24.39 +        case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
   24.40 +        case (None, Some(name)) => "file " + quote(name)
   24.41 +        case _ => ""
   24.42 +      })
   24.43  }
    25.1 --- a/src/Pure/Isar/keyword.ML	Mon Mar 16 15:30:00 2015 +0000
    25.2 +++ b/src/Pure/Isar/keyword.ML	Tue Mar 17 12:23:56 2015 +0000
    25.3 @@ -249,4 +249,3 @@
    25.4  fun is_printed keywords = is_theory_goal keywords orf is_proof keywords;
    25.5  
    25.6  end;
    25.7 -
    26.1 --- a/src/Pure/Isar/keyword.scala	Mon Mar 16 15:30:00 2015 +0000
    26.2 +++ b/src/Pure/Isar/keyword.scala	Tue Mar 17 12:23:56 2015 +0000
    26.3 @@ -39,7 +39,7 @@
    26.4    val PRF_SCRIPT = "prf_script"
    26.5  
    26.6  
    26.7 -  /* categories */
    26.8 +  /* command categories */
    26.9  
   26.10    val vacous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
   26.11  
   26.12 @@ -50,6 +50,11 @@
   26.13    val document_raw = Set(DOCUMENT_RAW)
   26.14    val document = Set(DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
   26.15  
   26.16 +  val theory_begin = Set(THY_BEGIN)
   26.17 +  val theory_end = Set(THY_END)
   26.18 +
   26.19 +  val theory_load = Set(THY_LOAD)
   26.20 +
   26.21    val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
   26.22  
   26.23    val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK)
   26.24 @@ -139,6 +144,12 @@
   26.25  
   26.26      def command_kind(name: String): Option[String] = commands.get(name).map(_._1)
   26.27  
   26.28 +    def is_command_kind(name: String, pred: String => Boolean): Boolean =
   26.29 +      command_kind(name) match {
   26.30 +        case Some(kind) => pred(kind)
   26.31 +        case None => false
   26.32 +      }
   26.33 +
   26.34  
   26.35      /* load commands */
   26.36  
   26.37 @@ -155,4 +166,3 @@
   26.38        load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
   26.39    }
   26.40  }
   26.41 -
    27.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Mar 16 15:30:00 2015 +0000
    27.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Mar 17 12:23:56 2015 +0000
    27.3 @@ -123,7 +123,9 @@
    27.4      }
    27.5  
    27.6  
    27.7 -  /* load commands */
    27.8 +  /* command categories */
    27.9 +
   27.10 +  def is_theory_begin(name: String): Boolean = keywords.is_command_kind(name, Keyword.theory_begin)
   27.11  
   27.12    def load_command(name: String): Option[List[String]] = keywords.load_command(name)
   27.13    def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
   27.14 @@ -235,7 +237,7 @@
   27.15        case "subsubsection" => Some(3)
   27.16        case _ =>
   27.17          keywords.command_kind(command.name) match {
   27.18 -          case Some(kind) if Keyword.theory(kind) && kind != Keyword.THY_END => Some(4)
   27.19 +          case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(4)
   27.20            case _ => None
   27.21          }
   27.22      }
   27.23 @@ -284,7 +286,7 @@
   27.24      /* result structure */
   27.25  
   27.26      val spans = parse_spans(text)
   27.27 -    spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
   27.28 +    spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span)))
   27.29      result()
   27.30    }
   27.31  }
    28.1 --- a/src/Pure/Isar/parse.ML	Mon Mar 16 15:30:00 2015 +0000
    28.2 +++ b/src/Pure/Isar/parse.ML	Tue Mar 17 12:23:56 2015 +0000
    28.3 @@ -69,6 +69,8 @@
    28.4    val xname: xstring parser
    28.5    val text: string parser
    28.6    val path: string parser
    28.7 +  val theory_name: bstring parser
    28.8 +  val theory_xname: xstring parser
    28.9    val liberal_name: xstring parser
   28.10    val parname: string parser
   28.11    val parbinding: binding parser
   28.12 @@ -275,6 +277,9 @@
   28.13  
   28.14  val path = group (fn () => "file name/path specification") name;
   28.15  
   28.16 +val theory_name = group (fn () => "theory name") name;
   28.17 +val theory_xname = group (fn () => "theory name reference") xname;
   28.18 +
   28.19  val liberal_name = keyword_with Token.ident_or_symbolic || xname;
   28.20  
   28.21  val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
    29.1 --- a/src/Pure/Isar/parse.scala	Mon Mar 16 15:30:00 2015 +0000
    29.2 +++ b/src/Pure/Isar/parse.scala	Tue Mar 17 12:23:56 2015 +0000
    29.3 @@ -25,31 +25,42 @@
    29.4        if (!filter_proper || in.atEnd || in.first.is_proper) in
    29.5        else proper(in.rest)
    29.6  
    29.7 -    def token(s: String, pred: Elem => Boolean): Parser[(Elem, Token.Pos)] =
    29.8 -      new Parser[(Elem, Token.Pos)] {
    29.9 +    private def proper_position: Parser[Position.T] =
   29.10 +      new Parser[Position.T] {
   29.11 +        def apply(raw_input: Input) =
   29.12 +        {
   29.13 +          val in = proper(raw_input)
   29.14 +          val pos =
   29.15 +            in.pos match {
   29.16 +              case pos: Token.Pos => pos
   29.17 +              case _ => Token.Pos.none
   29.18 +            }
   29.19 +          Success(if (in.atEnd) pos.position() else pos.position(in.first), in)
   29.20 +        }
   29.21 +      }
   29.22 +
   29.23 +    def position[A](parser: Parser[A]): Parser[(A, Position.T)] =
   29.24 +      proper_position ~ parser ^^ { case x ~ y => (y, x) }
   29.25 +
   29.26 +    def token(s: String, pred: Elem => Boolean): Parser[Elem] =
   29.27 +      new Parser[Elem] {
   29.28          def apply(raw_input: Input) =
   29.29          {
   29.30            val in = proper(raw_input)
   29.31            if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in)
   29.32            else {
   29.33 -            val pos =
   29.34 -              in.pos match {
   29.35 -                case pos: Token.Pos => pos
   29.36 -                case _ => Token.Pos.none
   29.37 -              }
   29.38              val token = in.first
   29.39 -            if (pred(token)) Success((token, pos), proper(in.rest))
   29.40 +            if (pred(token)) Success(token, proper(in.rest))
   29.41              else Failure(s + " expected,\nbut " + token.kind + " was found:\n" + token.source, in)
   29.42            }
   29.43          }
   29.44        }
   29.45  
   29.46      def atom(s: String, pred: Elem => Boolean): Parser[String] =
   29.47 -      token(s, pred) ^^ { case (tok, _) => tok.content }
   29.48 +      token(s, pred) ^^ (_.content)
   29.49  
   29.50 -    def command(name: String): Parser[Position.T] =
   29.51 -      token("command " + quote(name), tok => tok.is_command && tok.source == name) ^^
   29.52 -        { case (_, pos) => pos.position }
   29.53 +    def command(name: String): Parser[String] =
   29.54 +      atom("command " + quote(name), tok => tok.is_command && tok.source == name)
   29.55  
   29.56      def $$$(name: String): Parser[String] =
   29.57        atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)
   29.58 @@ -61,8 +72,10 @@
   29.59      def text: Parser[String] = atom("text", _.is_text)
   29.60      def ML_source: Parser[String] = atom("ML source", _.is_text)
   29.61      def document_source: Parser[String] = atom("document source", _.is_text)
   29.62 +
   29.63      def path: Parser[String] =
   29.64        atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
   29.65 +
   29.66      def theory_name: Parser[String] =
   29.67        atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))
   29.68      def theory_xname: Parser[String] =
    30.1 --- a/src/Pure/Isar/token.scala	Mon Mar 16 15:30:00 2015 +0000
    30.2 +++ b/src/Pure/Isar/token.scala	Tue Mar 17 12:23:56 2015 +0000
    30.3 @@ -157,10 +157,17 @@
    30.4  
    30.5    object Pos
    30.6    {
    30.7 -    val none: Pos = new Pos(0, "")
    30.8 +    val none: Pos = new Pos(0, 0, "", "")
    30.9 +    val start: Pos = new Pos(1, 1, "", "")
   30.10 +    def file(file: String): Pos = new Pos(1, 1, file, "")
   30.11 +    def id(id: String): Pos = new Pos(0, 1, "", id)
   30.12    }
   30.13  
   30.14 -  final class Pos private[Token](val line: Int, val file: String)
   30.15 +  final class Pos private[Token](
   30.16 +      val line: Int,
   30.17 +      val offset: Symbol.Offset,
   30.18 +      val file: String,
   30.19 +      val id: String)
   30.20      extends scala.util.parsing.input.Position
   30.21    {
   30.22      def column = 0
   30.23 @@ -168,13 +175,27 @@
   30.24  
   30.25      def advance(token: Token): Pos =
   30.26      {
   30.27 -      var n = 0
   30.28 -      for (c <- token.content if c == '\n') n += 1
   30.29 -      if (n == 0) this else new Pos(line + n, file)
   30.30 +      var line1 = line
   30.31 +      var offset1 = offset
   30.32 +      for (s <- Symbol.iterator(token.source)) {
   30.33 +        if (line1 > 0 && Symbol.is_newline(s)) line1 += 1
   30.34 +        if (offset1 > 0) offset1 += 1
   30.35 +      }
   30.36 +      if (line1 == line && offset1 == offset) this
   30.37 +      else new Pos(line1, offset1, file, id)
   30.38      }
   30.39  
   30.40 -    def position: Position.T = Position.Line_File(line, file)
   30.41 -    override def toString: String = Position.here_undelimited(position)
   30.42 +    private def position(end_offset: Symbol.Offset): Position.T =
   30.43 +      (if (line > 0) Position.Line(line) else Nil) :::
   30.44 +      (if (offset > 0) Position.Offset(offset) else Nil) :::
   30.45 +      (if (end_offset > 0) Position.End_Offset(end_offset) else Nil) :::
   30.46 +      (if (file != "") Position.File(file) else Nil) :::
   30.47 +      (if (id != "") Position.Id_String(id) else Nil)
   30.48 +
   30.49 +    def position(): Position.T = position(0)
   30.50 +    def position(token: Token): Position.T = position(advance(token).offset)
   30.51 +
   30.52 +    override def toString: String = Position.here_undelimited(position())
   30.53    }
   30.54  
   30.55    abstract class Reader extends scala.util.parsing.input.Reader[Token]
   30.56 @@ -186,8 +207,8 @@
   30.57      def atEnd = tokens.isEmpty
   30.58    }
   30.59  
   30.60 -  def reader(tokens: List[Token], file: String = ""): Reader =
   30.61 -    new Token_Reader(tokens, new Pos(1, file))
   30.62 +  def reader(tokens: List[Token], start: Token.Pos): Reader =
   30.63 +    new Token_Reader(tokens, start)
   30.64  }
   30.65  
   30.66  
   30.67 @@ -195,8 +216,7 @@
   30.68  {
   30.69    def is_command: Boolean = kind == Token.Kind.COMMAND
   30.70    def is_command_kind(keywords: Keyword.Keywords, pred: String => Boolean): Boolean =
   30.71 -    is_command &&
   30.72 -      (keywords.command_kind(source) match { case Some(k) => pred(k) case None => false })
   30.73 +    is_command && keywords.is_command_kind(source, pred)
   30.74    def is_keyword: Boolean = kind == Token.Kind.KEYWORD
   30.75    def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
   30.76    def is_ident: Boolean = kind == Token.Kind.IDENT
    31.1 --- a/src/Pure/PIDE/command.ML	Mon Mar 16 15:30:00 2015 +0000
    31.2 +++ b/src/Pure/PIDE/command.ML	Tue Mar 17 12:23:56 2015 +0000
    31.3 @@ -10,14 +10,14 @@
    31.4    val read_file: Path.T -> Position.T -> Path.T -> Token.file
    31.5    val read_thy: Toplevel.state -> theory
    31.6    val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
    31.7 -    blob list -> Token.T list -> Toplevel.transition
    31.8 +    blob list * int -> Token.T list -> Toplevel.transition
    31.9    type eval
   31.10    val eval_eq: eval * eval -> bool
   31.11    val eval_running: eval -> bool
   31.12    val eval_finished: eval -> bool
   31.13    val eval_result_state: eval -> Toplevel.state
   31.14    val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
   31.15 -    blob list -> Token.T list -> eval -> eval
   31.16 +    blob list * int -> Token.T list -> eval -> eval
   31.17    type print
   31.18    val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
   31.19      eval -> print list -> print list option
   31.20 @@ -51,21 +51,19 @@
   31.21  
   31.22  fun read_file_node file_node master_dir pos src_path =
   31.23    let
   31.24 -    val _ = Position.report pos Markup.language_path;
   31.25      val _ =
   31.26        (case try Url.explode file_node of
   31.27          NONE => ()
   31.28        | SOME (Url.File _) => ()
   31.29        | _ =>
   31.30 -         (Position.report pos (Markup.path file_node);
   31.31            error ("Prover cannot load remote file " ^
   31.32 -            Markup.markup (Markup.path file_node) (quote file_node) ^ Position.here pos)));
   31.33 +            Markup.markup (Markup.path file_node) (quote file_node)));
   31.34      val full_path = File.check_file (File.full_path master_dir src_path);
   31.35 -    val _ = Position.report pos (Markup.path (Path.implode full_path));
   31.36      val text = File.read full_path;
   31.37      val lines = split_lines text;
   31.38      val digest = SHA1.digest text;
   31.39 -  in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end;
   31.40 +  in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end
   31.41 +  handle ERROR msg => error (msg ^ Position.here pos);
   31.42  
   31.43  val read_file = read_file_node "";
   31.44  
   31.45 @@ -80,27 +78,33 @@
   31.46        | SOME exec_id => Position.put_id exec_id);
   31.47    in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
   31.48  
   31.49 -fun resolve_files keywords master_dir blobs toks =
   31.50 +fun resolve_files keywords master_dir (blobs, blobs_index) toks =
   31.51    (case Outer_Syntax.parse_spans toks of
   31.52 -    [span] => span
   31.53 -      |> Command_Span.resolve_files keywords (fn cmd => fn (path, pos) =>
   31.54 -        let
   31.55 -          fun make_file src_path (Exn.Res (file_node, NONE)) =
   31.56 -                Exn.interruptible_capture (fn () =>
   31.57 -                  read_file_node file_node master_dir pos src_path) ()
   31.58 -            | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
   31.59 -               (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)];
   31.60 -                Exn.Res (blob_file src_path lines digest file_node))
   31.61 -            | make_file _ (Exn.Exn e) = Exn.Exn e;
   31.62 -          val src_paths = Keyword.command_files keywords cmd path;
   31.63 -        in
   31.64 -          if null blobs then
   31.65 -            map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
   31.66 -          else if length src_paths = length blobs then
   31.67 -            map2 make_file src_paths blobs
   31.68 -          else error ("Misalignment of inlined files" ^ Position.here pos)
   31.69 -        end)
   31.70 -      |> Command_Span.content
   31.71 +    [Command_Span.Span (Command_Span.Command_Span (cmd, _), _)] =>
   31.72 +      (case try (nth toks) blobs_index of
   31.73 +        SOME tok =>
   31.74 +          let
   31.75 +            val pos = Token.pos_of tok;
   31.76 +            val path = Path.explode (Token.content_of tok)
   31.77 +              handle ERROR msg => error (msg ^ Position.here pos);
   31.78 +            fun make_file src_path (Exn.Res (file_node, NONE)) =
   31.79 +                  Exn.interruptible_capture (fn () =>
   31.80 +                    read_file_node file_node master_dir pos src_path) ()
   31.81 +              | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
   31.82 +                  Exn.Res (blob_file src_path lines digest file_node)
   31.83 +              | make_file _ (Exn.Exn e) = Exn.Exn e;
   31.84 +            val src_paths = Keyword.command_files keywords cmd path;
   31.85 +            val files =
   31.86 +              if null blobs then
   31.87 +                map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
   31.88 +              else if length src_paths = length blobs then
   31.89 +                map2 make_file src_paths blobs
   31.90 +              else error ("Misalignment of inlined files" ^ Position.here pos);
   31.91 +          in
   31.92 +            toks |> map_index (fn (i, tok) =>
   31.93 +              if i = blobs_index then Token.put_files files tok else tok)
   31.94 +          end
   31.95 +      | NONE => toks)
   31.96    | _ => toks);
   31.97  
   31.98  val bootstrap_thy = ML_Context.the_global_context ();
   31.99 @@ -109,7 +113,7 @@
  31.100  
  31.101  fun read_thy st = Toplevel.theory_of st handle Toplevel.UNDEF => bootstrap_thy;
  31.102  
  31.103 -fun read keywords thy master_dir init blobs span =
  31.104 +fun read keywords thy master_dir init blobs_info span =
  31.105    let
  31.106      val command_reports = Outer_Syntax.command_reports thy;
  31.107  
  31.108 @@ -124,7 +128,7 @@
  31.109    in
  31.110      if is_malformed then Toplevel.malformed pos "Malformed command syntax"
  31.111      else
  31.112 -      (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs span) of
  31.113 +      (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs_info span) of
  31.114          [tr] => Toplevel.modify_init init tr
  31.115        | [] => Toplevel.ignored (#1 (Token.range_of span))
  31.116        | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
  31.117 @@ -221,7 +225,7 @@
  31.118  
  31.119  in
  31.120  
  31.121 -fun eval keywords master_dir init blobs span eval0 =
  31.122 +fun eval keywords master_dir init blobs_info span eval0 =
  31.123    let
  31.124      val exec_id = Document_ID.make ();
  31.125      fun process () =
  31.126 @@ -230,7 +234,8 @@
  31.127          val thy = read_thy (#state eval_state0);
  31.128          val tr =
  31.129            Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
  31.130 -            (fn () => read keywords thy master_dir init blobs span |> Toplevel.exec_id exec_id) ();
  31.131 +            (fn () =>
  31.132 +              read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) ();
  31.133        in eval_state keywords span tr eval_state0 end;
  31.134    in Eval {exec_id = exec_id, eval_process = Lazy.lazy process} end;
  31.135  
    32.1 --- a/src/Pure/PIDE/command.scala	Mon Mar 16 15:30:00 2015 +0000
    32.2 +++ b/src/Pure/PIDE/command.scala	Tue Mar 17 12:23:56 2015 +0000
    32.3 @@ -10,13 +10,16 @@
    32.4  
    32.5  import scala.collection.mutable
    32.6  import scala.collection.immutable.SortedMap
    32.7 +import scala.util.parsing.input.CharSequenceReader
    32.8  
    32.9  
   32.10  object Command
   32.11  {
   32.12    type Edit = (Option[Command], Option[Command])
   32.13 +
   32.14    type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Symbol.Text_Chunk)])]
   32.15 -
   32.16 +  type Blobs_Info = (List[Blob], Int)
   32.17 +  val no_blobs: Blobs_Info = (Nil, -1)
   32.18  
   32.19  
   32.20    /** accumulated results from prover **/
   32.21 @@ -253,15 +256,15 @@
   32.22    def apply(
   32.23      id: Document_ID.Command,
   32.24      node_name: Document.Node.Name,
   32.25 -    blobs: List[Blob],
   32.26 +    blobs_info: Blobs_Info,
   32.27      span: Command_Span.Span): Command =
   32.28    {
   32.29      val (source, span1) = span.compact_source
   32.30 -    new Command(id, node_name, blobs, span1, source, Results.empty, Markup_Tree.empty)
   32.31 +    new Command(id, node_name, blobs_info, span1, source, Results.empty, Markup_Tree.empty)
   32.32    }
   32.33  
   32.34    val empty: Command =
   32.35 -    Command(Document_ID.none, Document.Node.Name.empty, Nil, Command_Span.empty)
   32.36 +    Command(Document_ID.none, Document.Node.Name.empty, no_blobs, Command_Span.empty)
   32.37  
   32.38    def unparsed(
   32.39      id: Document_ID.Command,
   32.40 @@ -270,7 +273,7 @@
   32.41      markup: Markup_Tree): Command =
   32.42    {
   32.43      val (source1, span1) = Command_Span.unparsed(source).compact_source
   32.44 -    new Command(id, Document.Node.Name.empty, Nil, span1, source1, results, markup)
   32.45 +    new Command(id, Document.Node.Name.empty, no_blobs, span1, source1, results, markup)
   32.46    }
   32.47  
   32.48    def unparsed(source: String): Command =
   32.49 @@ -305,13 +308,89 @@
   32.50          (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
   32.51      }
   32.52    }
   32.53 +
   32.54 +
   32.55 +  /* blobs: inlined errors and auxiliary files */
   32.56 +
   32.57 +  private def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
   32.58 +  {
   32.59 +    def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
   32.60 +      toks match {
   32.61 +        case (t1, i1) :: (t2, i2) :: rest =>
   32.62 +          if (t1.is_keyword && (t1.source == "%" || t1.source == "--")) clean(rest)
   32.63 +          else (t1, i1) :: clean((t2, i2) :: rest)
   32.64 +        case _ => toks
   32.65 +      }
   32.66 +    clean(tokens.zipWithIndex.filter({ case (t, _) => t.is_proper }))
   32.67 +  }
   32.68 +
   32.69 +  private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
   32.70 +    tokens match {
   32.71 +      case (tok, _) :: toks =>
   32.72 +        if (tok.is_command)
   32.73 +          toks.collectFirst({ case (t, i) if t.is_name => (t.content, i) })
   32.74 +        else None
   32.75 +      case Nil => None
   32.76 +    }
   32.77 +
   32.78 +  def span_files(syntax: Prover.Syntax, span: Command_Span.Span): (List[String], Int) =
   32.79 +    span.kind match {
   32.80 +      case Command_Span.Command_Span(name, _) =>
   32.81 +        syntax.load_command(name) match {
   32.82 +          case Some(exts) =>
   32.83 +            find_file(clean_tokens(span.content)) match {
   32.84 +              case Some((file, i)) =>
   32.85 +                if (exts.isEmpty) (List(file), i)
   32.86 +                else (exts.map(ext => file + "." + ext), i)
   32.87 +              case None => (Nil, -1)
   32.88 +            }
   32.89 +          case None => (Nil, -1)
   32.90 +        }
   32.91 +      case _ => (Nil, -1)
   32.92 +    }
   32.93 +
   32.94 +  def blobs_info(
   32.95 +    resources: Resources,
   32.96 +    syntax: Prover.Syntax,
   32.97 +    get_blob: Document.Node.Name => Option[Document.Blob],
   32.98 +    can_import: Document.Node.Name => Boolean,
   32.99 +    node_name: Document.Node.Name,
  32.100 +    span: Command_Span.Span): Blobs_Info =
  32.101 +  {
  32.102 +    span.kind match {
  32.103 +      // inlined errors
  32.104 +      case Command_Span.Command_Span(name, _) if syntax.is_theory_begin(name) =>
  32.105 +        val header =
  32.106 +          resources.check_thy_reader("", node_name,
  32.107 +            new CharSequenceReader(span.source), Token.Pos.id(Markup.COMMAND))
  32.108 +        val import_errors =
  32.109 +          for ((imp, pos) <- header.imports if !can_import(imp)) yield {
  32.110 +            val name = imp.node
  32.111 +            "Bad theory import " + Markup.Path(name).markup(quote(name)) + Position.here(pos)
  32.112 +          }
  32.113 +        ((header.errors ::: import_errors).map(msg => Exn.Exn(ERROR(msg)): Command.Blob), -1)
  32.114 +
  32.115 +      // auxiliary files
  32.116 +      case _ =>
  32.117 +        val (files, index) = span_files(syntax, span)
  32.118 +        val blobs =
  32.119 +          files.map(file =>
  32.120 +            (Exn.capture {
  32.121 +              val name =
  32.122 +                Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
  32.123 +              val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
  32.124 +              (name, blob)
  32.125 +            }).user_error)
  32.126 +        (blobs, index)
  32.127 +    }
  32.128 +  }
  32.129  }
  32.130  
  32.131  
  32.132  final class Command private(
  32.133      val id: Document_ID.Command,
  32.134      val node_name: Document.Node.Name,
  32.135 -    val blobs: List[Command.Blob],
  32.136 +    val blobs_info: Command.Blobs_Info,
  32.137      val span: Command_Span.Span,
  32.138      val source: String,
  32.139      val init_results: Command.Results,
  32.140 @@ -340,6 +419,9 @@
  32.141  
  32.142    /* blobs */
  32.143  
  32.144 +  def blobs: List[Command.Blob] = blobs_info._1
  32.145 +  def blobs_index: Int = blobs_info._2
  32.146 +
  32.147    def blobs_names: List[Document.Node.Name] =
  32.148      for (Exn.Res((name, _)) <- blobs) yield name
  32.149  
    33.1 --- a/src/Pure/PIDE/command_span.ML	Mon Mar 16 15:30:00 2015 +0000
    33.2 +++ b/src/Pure/PIDE/command_span.ML	Tue Mar 17 12:23:56 2015 +0000
    33.3 @@ -10,8 +10,6 @@
    33.4    datatype span = Span of kind * Token.T list
    33.5    val kind: span -> kind
    33.6    val content: span -> Token.T list
    33.7 -  val resolve_files: Keyword.keywords ->
    33.8 -    (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
    33.9  end;
   33.10  
   33.11  structure Command_Span: COMMAND_SPAN =
   33.12 @@ -23,49 +21,4 @@
   33.13  fun kind (Span (k, _)) = k;
   33.14  fun content (Span (_, toks)) = toks;
   33.15  
   33.16 -
   33.17 -(* resolve inlined files *)
   33.18 -
   33.19 -local
   33.20 -
   33.21 -fun clean ((i1, t1) :: (i2, t2) :: toks) =
   33.22 -      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
   33.23 -      else (i1, t1) :: clean ((i2, t2) :: toks)
   33.24 -  | clean toks = toks;
   33.25 -
   33.26 -fun clean_tokens toks =
   33.27 -  ((0 upto length toks - 1) ~~ toks)
   33.28 -  |> filter (fn (_, tok) => Token.is_proper tok)
   33.29 -  |> clean;
   33.30 -
   33.31 -fun find_file ((_, tok) :: toks) =
   33.32 -      if Token.is_command tok then
   33.33 -        toks |> get_first (fn (i, tok) =>
   33.34 -          if Token.is_name tok then
   33.35 -            SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
   33.36 -              handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
   33.37 -          else NONE)
   33.38 -      else NONE
   33.39 -  | find_file [] = NONE;
   33.40 -
   33.41 -in
   33.42 -
   33.43 -fun resolve_files keywords read_files span =
   33.44 -  (case span of
   33.45 -    Span (Command_Span (cmd, pos), toks) =>
   33.46 -      if Keyword.is_theory_load keywords cmd then
   33.47 -        (case find_file (clean_tokens toks) of
   33.48 -          NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
   33.49 -        | SOME (i, path) =>
   33.50 -            let
   33.51 -              val toks' = toks |> map_index (fn (j, tok) =>
   33.52 -                if i = j then Token.put_files (read_files cmd path) tok
   33.53 -                else tok);
   33.54 -            in Span (Command_Span (cmd, pos), toks') end)
   33.55 -      else span
   33.56 -  | _ => span);
   33.57 -
   33.58  end;
   33.59 -
   33.60 -end;
   33.61 -
    34.1 --- a/src/Pure/PIDE/command_span.scala	Mon Mar 16 15:30:00 2015 +0000
    34.2 +++ b/src/Pure/PIDE/command_span.scala	Tue Mar 17 12:23:56 2015 +0000
    34.3 @@ -28,23 +28,24 @@
    34.4    {
    34.5      def length: Int = (0 /: content)(_ + _.source.length)
    34.6  
    34.7 +    def source: String =
    34.8 +      content match {
    34.9 +        case List(tok) => tok.source
   34.10 +        case toks => toks.map(_.source).mkString
   34.11 +      }
   34.12 +
   34.13      def compact_source: (String, Span) =
   34.14      {
   34.15 -      val source: String =
   34.16 -        content match {
   34.17 -          case List(tok) => tok.source
   34.18 -          case toks => toks.map(_.source).mkString
   34.19 -        }
   34.20 -
   34.21 +      val src = source
   34.22        val content1 = new mutable.ListBuffer[Token]
   34.23        var i = 0
   34.24        for (Token(kind, s) <- content) {
   34.25          val n = s.length
   34.26 -        val s1 = source.substring(i, i + n)
   34.27 +        val s1 = src.substring(i, i + n)
   34.28          content1 += Token(kind, s1)
   34.29          i += n
   34.30        }
   34.31 -      (source, Span(kind, content1.toList))
   34.32 +      (src, Span(kind, content1.toList))
   34.33      }
   34.34    }
   34.35  
   34.36 @@ -52,55 +53,4 @@
   34.37  
   34.38    def unparsed(source: String): Span =
   34.39      Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
   34.40 -
   34.41 -
   34.42 -  /* resolve inlined files */
   34.43 -
   34.44 -  private def find_file(tokens: List[Token]): Option[String] =
   34.45 -  {
   34.46 -    def clean(toks: List[Token]): List[Token] =
   34.47 -      toks match {
   34.48 -        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
   34.49 -        case t :: ts => t :: clean(ts)
   34.50 -        case Nil => Nil
   34.51 -      }
   34.52 -    clean(tokens.filter(_.is_proper)) match {
   34.53 -      case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
   34.54 -      case _ => None
   34.55 -    }
   34.56 -  }
   34.57 -
   34.58 -  def span_files(syntax: Prover.Syntax, span: Span): List[String] =
   34.59 -    span.kind match {
   34.60 -      case Command_Span(name, _) =>
   34.61 -        syntax.load_command(name) match {
   34.62 -          case Some(exts) =>
   34.63 -            find_file(span.content) match {
   34.64 -              case Some(file) =>
   34.65 -                if (exts.isEmpty) List(file)
   34.66 -                else exts.map(ext => file + "." + ext)
   34.67 -              case None => Nil
   34.68 -            }
   34.69 -          case None => Nil
   34.70 -        }
   34.71 -      case _ => Nil
   34.72 -    }
   34.73 -
   34.74 -  def resolve_files(
   34.75 -      resources: Resources,
   34.76 -      syntax: Prover.Syntax,
   34.77 -      node_name: Document.Node.Name,
   34.78 -      span: Span,
   34.79 -      get_blob: Document.Node.Name => Option[Document.Blob])
   34.80 -    : List[Command.Blob] =
   34.81 -  {
   34.82 -    span_files(syntax, span).map(file_name =>
   34.83 -      Exn.capture {
   34.84 -        val name =
   34.85 -          Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
   34.86 -        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
   34.87 -        (name, blob)
   34.88 -      })
   34.89 -  }
   34.90  }
   34.91 -
    35.1 --- a/src/Pure/PIDE/document.ML	Mon Mar 16 15:30:00 2015 +0000
    35.2 +++ b/src/Pure/PIDE/document.ML	Tue Mar 17 12:23:56 2015 +0000
    35.3 @@ -19,7 +19,7 @@
    35.4    val init_state: state
    35.5    val define_blob: string -> string -> state -> state
    35.6    type blob_digest = (string * string option) Exn.result
    35.7 -  val define_command: Document_ID.command -> string -> blob_digest list ->
    35.8 +  val define_command: Document_ID.command -> string -> blob_digest list -> int ->
    35.9      ((int * int) * string) list -> state -> state
   35.10    val remove_versions: Document_ID.version list -> state -> state
   35.11    val start_execution: state -> state
   35.12 @@ -307,8 +307,8 @@
   35.13  abstype state = State of
   35.14   {versions: version Inttab.table,  (*version id -> document content*)
   35.15    blobs: (SHA1.digest * string list) Symtab.table,  (*raw digest -> digest, lines*)
   35.16 -  commands: (string * blob_digest list * Token.T list lazy) Inttab.table,
   35.17 -    (*command id -> name, inlined files, command span*)
   35.18 +  commands: (string * blob_digest list * int * Token.T list lazy) Inttab.table,
   35.19 +    (*command id -> name, inlined files, token index of files, command span*)
   35.20    execution: execution}  (*current execution process*)
   35.21  with
   35.22  
   35.23 @@ -359,23 +359,39 @@
   35.24    blob_digest |> Exn.map_result (fn (file_node, raw_digest) =>
   35.25      (file_node, Option.map (the_blob state) raw_digest));
   35.26  
   35.27 +fun blob_reports pos (blob_digest: blob_digest) =
   35.28 +  (case blob_digest of Exn.Res (file_node, _) => [(pos, Markup.path file_node)] | _ => []);
   35.29 +
   35.30  
   35.31  (* commands *)
   35.32  
   35.33 -fun define_command command_id name command_blobs toks =
   35.34 +fun define_command command_id name blobs_digests blobs_index toks =
   35.35    map_state (fn (versions, blobs, commands, execution) =>
   35.36      let
   35.37        val id = Document_ID.print command_id;
   35.38        val span =
   35.39          Lazy.lazy (fn () =>
   35.40            Position.setmp_thread_data (Position.id_only id)
   35.41 -            (fn () => #1 (fold_map Token.make toks (Position.id id))) ());
   35.42 +            (fn () =>
   35.43 +              let
   35.44 +                val (tokens, _) = fold_map Token.make toks (Position.id id);
   35.45 +                val _ =
   35.46 +                  if blobs_index < 0
   35.47 +                  then (*inlined errors*)
   35.48 +                    map_filter Exn.get_exn blobs_digests
   35.49 +                    |> List.app (Output.error_message o Runtime.exn_message)
   35.50 +                  else (*auxiliary files*)
   35.51 +                    let val pos = Token.pos_of (nth tokens blobs_index) in
   35.52 +                      Position.reports
   35.53 +                        ((pos, Markup.language_path) :: maps (blob_reports pos) blobs_digests)
   35.54 +                    end;
   35.55 +              in tokens end) ());
   35.56 +      val commands' =
   35.57 +        Inttab.update_new (command_id, (name, blobs_digests, blobs_index, span)) commands
   35.58 +          handle Inttab.DUP dup => err_dup "command" dup;
   35.59        val _ =
   35.60          Position.setmp_thread_data (Position.id_only id)
   35.61            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
   35.62 -      val commands' =
   35.63 -        Inttab.update_new (command_id, (name, command_blobs, span)) commands
   35.64 -          handle Inttab.DUP dup => err_dup "command" dup;
   35.65      in (versions, blobs, commands', execution) end);
   35.66  
   35.67  fun the_command (State {commands, ...}) command_id =
   35.68 @@ -405,7 +421,7 @@
   35.69                SOME o Inttab.insert (K true) (command_id, the_command state command_id))));
   35.70      val blobs' =
   35.71        (commands', Symtab.empty) |->
   35.72 -        Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
   35.73 +        Inttab.fold (fn (_, (_, blobs, _, _)) => blobs |>
   35.74            fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
   35.75  
   35.76    in (versions', blobs', commands', execution) end);
   35.77 @@ -571,13 +587,13 @@
   35.78  
   35.79        val command_visible = visible_command node command_id';
   35.80        val command_overlays = overlays node command_id';
   35.81 -      val (command_name, blob_digests, span0) = the_command state command_id';
   35.82 +      val (command_name, blob_digests, blobs_index, span0) = the_command state command_id';
   35.83        val blobs = map (resolve_blob state) blob_digests;
   35.84        val span = Lazy.force span0;
   35.85  
   35.86        val eval' =
   35.87          Command.eval keywords (master_directory node)
   35.88 -          (fn () => the_default illegal_init init span) blobs span eval;
   35.89 +          (fn () => the_default illegal_init init span) (blobs, blobs_index) span eval;
   35.90        val prints' =
   35.91          perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
   35.92        val exec' = (eval', prints');
    36.1 --- a/src/Pure/PIDE/document.scala	Mon Mar 16 15:30:00 2015 +0000
    36.2 +++ b/src/Pure/PIDE/document.scala	Tue Mar 17 12:23:56 2015 +0000
    36.3 @@ -81,7 +81,7 @@
    36.4      /* header and name */
    36.5  
    36.6      sealed case class Header(
    36.7 -      imports: List[Name],
    36.8 +      imports: List[(Name, Position.T)],
    36.9        keywords: Thy_Header.Keywords,
   36.10        errors: List[String])
   36.11      {
   36.12 @@ -256,6 +256,8 @@
   36.13        Node.is_no_perspective_command(perspective) &&
   36.14        commands.isEmpty
   36.15  
   36.16 +    def has_header: Boolean = header != Node.no_header
   36.17 +
   36.18      def commands: Linear_Set[Command] = _commands.commands
   36.19      def load_commands: List[Command] = _commands.load_commands
   36.20  
   36.21 @@ -323,7 +325,7 @@
   36.22      def + (entry: (Node.Name, Node)): Nodes =
   36.23      {
   36.24        val (name, node) = entry
   36.25 -      val imports = node.header.imports
   36.26 +      val imports = node.header.imports.map(_._1)
   36.27        val graph1 =
   36.28          (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
   36.29        val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
    37.1 --- a/src/Pure/PIDE/markup.scala	Mon Mar 16 15:30:00 2015 +0000
    37.2 +++ b/src/Pure/PIDE/markup.scala	Tue Mar 17 12:23:56 2015 +0000
    37.3 @@ -504,4 +504,7 @@
    37.4  
    37.5  
    37.6  sealed case class Markup(name: String, properties: Properties.T)
    37.7 -
    37.8 +{
    37.9 +  def markup(s: String): String =
   37.10 +    YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
   37.11 +}
    38.1 --- a/src/Pure/PIDE/protocol.ML	Mon Mar 16 15:30:00 2015 +0000
    38.2 +++ b/src/Pure/PIDE/protocol.ML	Tue Mar 17 12:23:56 2015 +0000
    38.3 @@ -30,17 +30,20 @@
    38.4    Isabelle_Process.protocol_command "Document.define_command"
    38.5      (fn id :: name :: blobs_yxml :: toks_yxml :: sources =>
    38.6        let
    38.7 -        val blobs =
    38.8 +        val (blobs, blobs_index) =
    38.9            YXML.parse_body blobs_yxml |>
   38.10              let open XML.Decode in
   38.11 -              list (variant
   38.12 -               [fn ([], a) => Exn.Res (pair string (option string) a),
   38.13 -                fn ([], a) => Exn.Exn (ERROR (string a))])
   38.14 +              pair
   38.15 +                (list (variant
   38.16 +                 [fn ([], a) => Exn.Res (pair string (option string) a),
   38.17 +                  fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))]))
   38.18 +                int
   38.19              end;
   38.20          val toks =
   38.21            (YXML.parse_body toks_yxml |> let open XML.Decode in list (pair int int) end) ~~ sources;
   38.22        in
   38.23 -        Document.change_state (Document.define_command (Document_ID.parse id) name blobs toks)
   38.24 +        Document.change_state
   38.25 +          (Document.define_command (Document_ID.parse id) name blobs blobs_index toks)
   38.26        end);
   38.27  
   38.28  val _ =
   38.29 @@ -72,7 +75,7 @@
   38.30                            pair string (pair string (pair (list string)
   38.31                              (pair (list (pair string
   38.32                                (option (pair (pair string (list string)) (list string)))))
   38.33 -                              (list string)))) a;
   38.34 +                              (list YXML.string_of_body)))) a;
   38.35                          val imports' = map (rpair Position.none) imports;
   38.36                          val header = Thy_Header.make (name, Position.none) imports' keywords;
   38.37                        in Document.Deps (master, header, errors) end,
    39.1 --- a/src/Pure/PIDE/protocol.scala	Mon Mar 16 15:30:00 2015 +0000
    39.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Mar 17 12:23:56 2015 +0000
    39.3 @@ -382,7 +382,30 @@
    39.4    def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
    39.5      protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
    39.6  
    39.7 -  def define_command(command: Command): Unit =
    39.8 +  private def resolve_id(id: String, body: XML.Body): XML.Body =
    39.9 +  {
   39.10 +    def resolve_property(p: (String, String)): (String, String) =
   39.11 +      if (p._1 == Markup.ID && p._2 == Markup.COMMAND) (Markup.ID, id) else p
   39.12 +
   39.13 +    def resolve_markup(markup: Markup): Markup =
   39.14 +      Markup(markup.name, markup.properties.map(resolve_property))
   39.15 +
   39.16 +    def resolve_tree(t: XML.Tree): XML.Tree =
   39.17 +      t match {
   39.18 +        case XML.Wrapped_Elem(markup, ts1, ts2) =>
   39.19 +          XML.Wrapped_Elem(resolve_markup(markup), ts1.map(resolve_tree _), ts2.map(resolve_tree _))
   39.20 +        case XML.Elem(markup, ts) =>
   39.21 +          XML.Elem(resolve_markup(markup), ts.map(resolve_tree _))
   39.22 +        case text => text
   39.23 +      }
   39.24 +    body.map(resolve_tree _)
   39.25 +  }
   39.26 +
   39.27 +  private def resolve_id(id: String, s: String): XML.Body =
   39.28 +    try { resolve_id(id, YXML.parse_body(s)) }
   39.29 +    catch { case ERROR(_) => XML.Encode.string(s) }
   39.30 +
   39.31 +  def define_command(command: Command)
   39.32    {
   39.33      val blobs_yxml =
   39.34      { import XML.Encode._
   39.35 @@ -390,9 +413,9 @@
   39.36          variant(List(
   39.37            { case Exn.Res((a, b)) =>
   39.38                (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
   39.39 -          { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
   39.40 +          { case Exn.Exn(e) => (Nil, resolve_id(command.id.toString, Exn.message(e))) }))
   39.41  
   39.42 -      YXML.string_of_body(list(encode_blob)(command.blobs))
   39.43 +      YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
   39.44      }
   39.45  
   39.46      val toks = command.span.content
   39.47 @@ -433,7 +456,7 @@
   39.48            { case Document.Node.Deps(header) =>
   39.49                val master_dir = Isabelle_System.posix_path_url(name.master_dir)
   39.50                val theory = Long_Name.base_name(name.theory)
   39.51 -              val imports = header.imports.map(_.node)
   39.52 +              val imports = header.imports.map({ case (a, _) => a.node })
   39.53                val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
   39.54                (Nil,
   39.55                  pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
    40.1 --- a/src/Pure/PIDE/prover.scala	Mon Mar 16 15:30:00 2015 +0000
    40.2 +++ b/src/Pure/PIDE/prover.scala	Tue Mar 17 12:23:56 2015 +0000
    40.3 @@ -20,6 +20,7 @@
    40.4      def ++ (other: Syntax): Syntax
    40.5      def add_keywords(keywords: Thy_Header.Keywords): Syntax
    40.6      def parse_spans(input: CharSequence): List[Command_Span.Span]
    40.7 +    def is_theory_begin(name: String): Boolean
    40.8      def load_command(name: String): Option[List[String]]
    40.9      def load_commands_in(text: String): Boolean
   40.10    }
    41.1 --- a/src/Pure/PIDE/resources.ML	Mon Mar 16 15:30:00 2015 +0000
    41.2 +++ b/src/Pure/PIDE/resources.ML	Tue Mar 17 12:23:56 2015 +0000
    41.3 @@ -128,7 +128,7 @@
    41.4    let
    41.5      fun prepare_span st span =
    41.6        Command_Span.content span
    41.7 -      |> Command.read keywords (Command.read_thy st) master_dir init []
    41.8 +      |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1)
    41.9        |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
   41.10  
   41.11      fun element_result span_elem (st, _) =
    42.1 --- a/src/Pure/PIDE/resources.scala	Mon Mar 16 15:30:00 2015 +0000
    42.2 +++ b/src/Pure/PIDE/resources.scala	Tue Mar 17 12:23:56 2015 +0000
    42.3 @@ -57,7 +57,7 @@
    42.4    def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
    42.5      if (syntax.load_commands_in(text)) {
    42.6        val spans = syntax.parse_spans(text)
    42.7 -      spans.iterator.map(Command_Span.span_files(syntax, _)).flatten.toList
    42.8 +      spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList
    42.9      }
   42.10      else Nil
   42.11  
   42.12 @@ -86,20 +86,21 @@
   42.13      }
   42.14    }
   42.15  
   42.16 -  def check_thy_reader(qualifier: String, name: Document.Node.Name, reader: Reader[Char])
   42.17 -    : Document.Node.Header =
   42.18 +  def check_thy_reader(qualifier: String, node_name: Document.Node.Name,
   42.19 +    reader: Reader[Char], start: Token.Pos): Document.Node.Header =
   42.20    {
   42.21      if (reader.source.length > 0) {
   42.22        try {
   42.23 -        val header = Thy_Header.read(reader).decode_symbols
   42.24 +        val header = Thy_Header.read(reader, start).decode_symbols
   42.25  
   42.26 -        val base_name = Long_Name.base_name(name.theory)
   42.27 -        val name1 = header.name
   42.28 -        if (base_name != name1)
   42.29 +        val base_name = Long_Name.base_name(node_name.theory)
   42.30 +        val (name, pos) = header.name
   42.31 +        if (base_name != name)
   42.32            error("Bad file name " + Resources.thy_path(Path.basic(base_name)) +
   42.33 -            " for theory " + quote(name1))
   42.34 +            " for theory " + quote(name) + Position.here(pos))
   42.35  
   42.36 -        val imports = header.imports.map(import_name(qualifier, name, _))
   42.37 +        val imports =
   42.38 +          header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
   42.39          Document.Node.Header(imports, header.keywords, Nil)
   42.40        }
   42.41        catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
   42.42 @@ -107,8 +108,16 @@
   42.43      else Document.Node.no_header
   42.44    }
   42.45  
   42.46 -  def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header =
   42.47 -    with_thy_reader(name, check_thy_reader(qualifier, name, _))
   42.48 +  def check_thy(qualifier: String, name: Document.Node.Name, start: Token.Pos)
   42.49 +    : Document.Node.Header =
   42.50 +    with_thy_reader(name, check_thy_reader(qualifier, name, _, start))
   42.51 +
   42.52 +  def check_file(file: String): Boolean =
   42.53 +    try {
   42.54 +      if (Url.is_wellformed(file)) Url.is_readable(file)
   42.55 +      else (new JFile(file)).isFile
   42.56 +    }
   42.57 +    catch { case ERROR(_) => false }
   42.58  
   42.59  
   42.60    /* document changes */
    43.1 --- a/src/Pure/System/options.scala	Mon Mar 16 15:30:00 2015 +0000
    43.2 +++ b/src/Pure/System/options.scala	Tue Mar 17 12:23:56 2015 +0000
    43.3 @@ -93,9 +93,9 @@
    43.4      {
    43.5        command(SECTION) ~! text ^^
    43.6          { case _ ~ a => (options: Options) => options.set_section(a) } |
    43.7 -      opt(command(PUBLIC)) ~ command(OPTION) ~! (option_name ~ $$$(":") ~ option_type ~
    43.8 +      opt(command(PUBLIC)) ~ position(command(OPTION)) ~! (option_name ~ $$$(":") ~ option_type ~
    43.9        $$$("=") ~ option_value ~ ($$$("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
   43.10 -        { case a ~ pos ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
   43.11 +        { case a ~ ((_, pos)) ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
   43.12              (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
   43.13      }
   43.14  
   43.15 @@ -110,7 +110,7 @@
   43.16      {
   43.17        val toks = Token.explode(syntax.keywords, File.read(file))
   43.18        val ops =
   43.19 -        parse_all(rep(parser), Token.reader(toks, file.implode)) match {
   43.20 +        parse_all(rep(parser), Token.reader(toks, Token.Pos.file(file.implode))) match {
   43.21            case Success(result, _) => result
   43.22            case bad => error(bad.toString)
   43.23          }
    44.1 --- a/src/Pure/Thy/thy_header.ML	Mon Mar 16 15:30:00 2015 +0000
    44.2 +++ b/src/Pure/Thy/thy_header.ML	Tue Mar 17 12:23:56 2015 +0000
    44.3 @@ -103,10 +103,9 @@
    44.4  
    44.5  local
    44.6  
    44.7 -val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name);
    44.8 -val theory_xname = Parse.group (fn () => "theory name reference") (Parse.position Parse.xname);
    44.9 -
   44.10 -val imports = Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_xname);
   44.11 +fun imports name =
   44.12 +  if name = Context.PureN then Scan.succeed []
   44.13 +  else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_xname));
   44.14  
   44.15  val opt_files =
   44.16    Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
   44.17 @@ -129,8 +128,8 @@
   44.18  in
   44.19  
   44.20  val args =
   44.21 -  theory_name :|-- (fn (name, pos) =>
   44.22 -    (if name = Context.PureN then Scan.succeed [] else imports) --
   44.23 +  Parse.position Parse.theory_name :|-- (fn (name, pos) =>
   44.24 +    imports name --
   44.25      Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
   44.26      Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords));
   44.27  
    45.1 --- a/src/Pure/Thy/thy_header.scala	Mon Mar 16 15:30:00 2015 +0000
    45.2 +++ b/src/Pure/Thy/thy_header.scala	Tue Mar 17 12:23:56 2015 +0000
    45.3 @@ -80,11 +80,10 @@
    45.4  
    45.5    val header: Parser[Thy_Header] =
    45.6    {
    45.7 -    val file_name = atom("file name", _.is_name)
    45.8 -
    45.9      val opt_files =
   45.10        $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } |
   45.11        success(Nil)
   45.12 +
   45.13      val keyword_spec =
   45.14        atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
   45.15        { case x ~ y ~ z => ((x, y), z) }
   45.16 @@ -94,17 +93,14 @@
   45.17        opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
   45.18        opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
   45.19        { case xs ~ y ~ z => xs.map((_, y, z)) }
   45.20 +
   45.21      val keyword_decls =
   45.22        keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
   45.23        { case xs ~ yss => (xs :: yss).flatten }
   45.24  
   45.25 -    val file =
   45.26 -      $$$("(") ~! (file_name ~ $$$(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
   45.27 -      file_name ^^ (x => (x, true))
   45.28 -
   45.29      val args =
   45.30 -      theory_name ~
   45.31 -      (opt($$$(IMPORTS) ~! (rep1(theory_xname))) ^^
   45.32 +      position(theory_name) ~
   45.33 +      (opt($$$(IMPORTS) ~! (rep1(position(theory_xname)))) ^^
   45.34          { case None => Nil case Some(_ ~ xs) => xs }) ~
   45.35        (opt($$$(KEYWORDS) ~! keyword_decls) ^^
   45.36          { case None => Nil case Some(_ ~ xs) => xs }) ~
   45.37 @@ -128,7 +124,7 @@
   45.38  
   45.39    /* read -- lazy scanning */
   45.40  
   45.41 -  def read(reader: Reader[Char]): Thy_Header =
   45.42 +  def read(reader: Reader[Char], start: Token.Pos): Thy_Header =
   45.43    {
   45.44      val token = Token.Parsers.token(bootstrap_keywords)
   45.45      val toks = new mutable.ListBuffer[Token]
   45.46 @@ -144,31 +140,27 @@
   45.47      }
   45.48      scan_to_begin(reader)
   45.49  
   45.50 -    parse(commit(header), Token.reader(toks.toList)) match {
   45.51 +    parse(commit(header), Token.reader(toks.toList, start)) match {
   45.52        case Success(result, _) => result
   45.53        case bad => error(bad.toString)
   45.54      }
   45.55    }
   45.56  
   45.57 -  def read(source: CharSequence): Thy_Header =
   45.58 -    read(new CharSequenceReader(source))
   45.59 +  def read(source: CharSequence, start: Token.Pos): Thy_Header =
   45.60 +    read(new CharSequenceReader(source), start)
   45.61  }
   45.62  
   45.63  
   45.64  sealed case class Thy_Header(
   45.65 -  name: String,
   45.66 -  imports: List[String],
   45.67 +  name: (String, Position.T),
   45.68 +  imports: List[(String, Position.T)],
   45.69    keywords: Thy_Header.Keywords)
   45.70  {
   45.71 -  def map(f: String => String): Thy_Header =
   45.72 -    Thy_Header(f(name), imports.map(f), keywords)
   45.73 -
   45.74    def decode_symbols: Thy_Header =
   45.75    {
   45.76      val f = Symbol.decode _
   45.77 -    Thy_Header(f(name), imports.map(f),
   45.78 +    Thy_Header((f(name._1), name._2), imports.map({ case (a, b) => (f(a), b) }),
   45.79        keywords.map({ case (a, b, c) =>
   45.80          (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f)) }), c.map(f)) }))
   45.81    }
   45.82  }
   45.83 -
    46.1 --- a/src/Pure/Thy/thy_info.scala	Mon Mar 16 15:30:00 2015 +0000
    46.2 +++ b/src/Pure/Thy/thy_info.scala	Tue Mar 17 12:23:56 2015 +0000
    46.3 @@ -106,7 +106,7 @@
    46.4            if (parent_loaded(dep.name.theory)) g
    46.5            else {
    46.6              val a = node(dep.name)
    46.7 -            val bs = dep.header.imports.map(node _)
    46.8 +            val bs = dep.header.imports.map({ case (name, _) => node(name) })
    46.9              ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
   46.10            }
   46.11        }
   46.12 @@ -134,10 +134,9 @@
   46.13        try {
   46.14          if (initiators.contains(name)) error(cycle_msg(initiators))
   46.15          val header =
   46.16 -          try { resources.check_thy(session, name).cat_errors(message) }
   46.17 +          try { resources.check_thy(session, name, Token.Pos.file(name.node)).cat_errors(message) }
   46.18            catch { case ERROR(msg) => cat_error(msg, message) }
   46.19 -        val imports = header.imports.map((_, Position.File(name.node)))
   46.20 -        Dep(name, header) :: require_thys(session, name :: initiators, required1, imports)
   46.21 +        Dep(name, header) :: require_thys(session, name :: initiators, required1, header.imports)
   46.22        }
   46.23        catch {
   46.24          case e: Throwable =>
    47.1 --- a/src/Pure/Thy/thy_syntax.scala	Mon Mar 16 15:30:00 2015 +0000
    47.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Mar 17 12:23:56 2015 +0000
    47.3 @@ -63,7 +63,7 @@
    47.4  
    47.5  
    47.6  
    47.7 -  /** header edits: structure and outer syntax **/
    47.8 +  /** header edits: graph structure and outer syntax **/
    47.9  
   47.10    private def header_edits(
   47.11      resources: Resources,
   47.12 @@ -82,7 +82,7 @@
   47.13            node.header.errors.nonEmpty || header.errors.nonEmpty || node.header != header
   47.14          if (update_header) {
   47.15            val node1 = node.update_header(header)
   47.16 -          if (node.header.imports != node1.header.imports ||
   47.17 +          if (node.header.imports.map(_._1) != node1.header.imports.map(_._1) ||
   47.18                node.header.keywords != node1.header.keywords) syntax_changed0 += name
   47.19            nodes += (name -> node1)
   47.20            doc_edits += (name -> Document.Node.Deps(header))
   47.21 @@ -98,7 +98,7 @@
   47.22          if (node.is_empty) None
   47.23          else {
   47.24            val header = node.header
   47.25 -          val imports_syntax = header.imports.flatMap(a => nodes(a).syntax)
   47.26 +          val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
   47.27            Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(header.keywords))
   47.28          }
   47.29        nodes += (name -> node.update_syntax(syntax))
   47.30 @@ -143,8 +143,8 @@
   47.31  
   47.32    @tailrec private def chop_common(
   47.33        cmds: List[Command],
   47.34 -      blobs_spans: List[(List[Command.Blob], Command_Span.Span)])
   47.35 -    : (List[Command], List[(List[Command.Blob], Command_Span.Span)]) =
   47.36 +      blobs_spans: List[(Command.Blobs_Info, Command_Span.Span)])
   47.37 +    : (List[Command], List[(Command.Blobs_Info, Command_Span.Span)]) =
   47.38    {
   47.39      (cmds, blobs_spans) match {
   47.40        case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
   47.41 @@ -157,14 +157,15 @@
   47.42      resources: Resources,
   47.43      syntax: Prover.Syntax,
   47.44      get_blob: Document.Node.Name => Option[Document.Blob],
   47.45 -    name: Document.Node.Name,
   47.46 +    can_import: Document.Node.Name => Boolean,
   47.47 +    node_name: Document.Node.Name,
   47.48      commands: Linear_Set[Command],
   47.49      first: Command, last: Command): Linear_Set[Command] =
   47.50    {
   47.51      val cmds0 = commands.iterator(first, last).toList
   47.52      val blobs_spans0 =
   47.53 -      syntax.parse_spans(cmds0.iterator.map(_.source).mkString).
   47.54 -        map(span => (Command_Span.resolve_files(resources, syntax, name, span, get_blob), span))
   47.55 +      syntax.parse_spans(cmds0.iterator.map(_.source).mkString).map(span =>
   47.56 +        (Command.blobs_info(resources, syntax, get_blob, can_import, node_name, span), span))
   47.57  
   47.58      val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
   47.59  
   47.60 @@ -179,75 +180,13 @@
   47.61        case cmd :: _ =>
   47.62          val hook = commands.prev(cmd)
   47.63          val inserted =
   47.64 -          blobs_spans2.map({ case (blobs, span) => Command(Document_ID.make(), name, blobs, span) })
   47.65 +          blobs_spans2.map({ case (blobs, span) =>
   47.66 +            Command(Document_ID.make(), node_name, blobs, span) })
   47.67          (commands /: cmds2)(_ - _).append_after(hook, inserted)
   47.68      }
   47.69    }
   47.70  
   47.71  
   47.72 -  /* recover command spans after edits */
   47.73 -
   47.74 -  // FIXME somewhat slow
   47.75 -  private def recover_spans(
   47.76 -    resources: Resources,
   47.77 -    syntax: Prover.Syntax,
   47.78 -    get_blob: Document.Node.Name => Option[Document.Blob],
   47.79 -    name: Document.Node.Name,
   47.80 -    perspective: Command.Perspective,
   47.81 -    commands: Linear_Set[Command]): Linear_Set[Command] =
   47.82 -  {
   47.83 -    val visible = perspective.commands.toSet
   47.84 -
   47.85 -    def next_invisible_command(cmds: Linear_Set[Command], from: Command): Command =
   47.86 -      cmds.iterator(from).dropWhile(cmd => !cmd.is_proper || visible(cmd))
   47.87 -        .find(_.is_proper) getOrElse cmds.last
   47.88 -
   47.89 -    @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] =
   47.90 -      cmds.find(_.is_unparsed) match {
   47.91 -        case Some(first_unparsed) =>
   47.92 -          val first = next_invisible_command(cmds.reverse, first_unparsed)
   47.93 -          val last = next_invisible_command(cmds, first_unparsed)
   47.94 -          recover(reparse_spans(resources, syntax, get_blob, name, cmds, first, last))
   47.95 -        case None => cmds
   47.96 -      }
   47.97 -    recover(commands)
   47.98 -  }
   47.99 -
  47.100 -
  47.101 -  /* consolidate unfinished spans */
  47.102 -
  47.103 -  private def consolidate_spans(
  47.104 -    resources: Resources,
  47.105 -    syntax: Prover.Syntax,
  47.106 -    get_blob: Document.Node.Name => Option[Document.Blob],
  47.107 -    reparse_limit: Int,
  47.108 -    name: Document.Node.Name,
  47.109 -    perspective: Command.Perspective,
  47.110 -    commands: Linear_Set[Command]): Linear_Set[Command] =
  47.111 -  {
  47.112 -    if (perspective.commands.isEmpty) commands
  47.113 -    else {
  47.114 -      commands.find(_.is_unfinished) match {
  47.115 -        case Some(first_unfinished) =>
  47.116 -          val visible = perspective.commands.toSet
  47.117 -          commands.reverse.find(visible) match {
  47.118 -            case Some(last_visible) =>
  47.119 -              val it = commands.iterator(last_visible)
  47.120 -              var last = last_visible
  47.121 -              var i = 0
  47.122 -              while (i < reparse_limit && it.hasNext) {
  47.123 -                last = it.next
  47.124 -                i += last.length
  47.125 -              }
  47.126 -              reparse_spans(resources, syntax, get_blob, name, commands, first_unfinished, last)
  47.127 -            case None => commands
  47.128 -          }
  47.129 -        case None => commands
  47.130 -      }
  47.131 -    }
  47.132 -  }
  47.133 -
  47.134 -
  47.135    /* main */
  47.136  
  47.137    def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command])
  47.138 @@ -264,9 +203,35 @@
  47.139      resources: Resources,
  47.140      syntax: Prover.Syntax,
  47.141      get_blob: Document.Node.Name => Option[Document.Blob],
  47.142 +    can_import: Document.Node.Name => Boolean,
  47.143      reparse_limit: Int,
  47.144      node: Document.Node, edit: Document.Edit_Text): Document.Node =
  47.145    {
  47.146 +    /* recover command spans after edits */
  47.147 +    // FIXME somewhat slow
  47.148 +    def recover_spans(
  47.149 +      name: Document.Node.Name,
  47.150 +      perspective: Command.Perspective,
  47.151 +      commands: Linear_Set[Command]): Linear_Set[Command] =
  47.152 +    {
  47.153 +      val is_visible = perspective.commands.toSet
  47.154 +
  47.155 +      def next_invisible(cmds: Linear_Set[Command], from: Command): Command =
  47.156 +        cmds.iterator(from).dropWhile(cmd => !cmd.is_proper || is_visible(cmd))
  47.157 +          .find(_.is_proper) getOrElse cmds.last
  47.158 +
  47.159 +      @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] =
  47.160 +        cmds.find(_.is_unparsed) match {
  47.161 +          case Some(first_unparsed) =>
  47.162 +            val first = next_invisible(cmds.reverse, first_unparsed)
  47.163 +            val last = next_invisible(cmds, first_unparsed)
  47.164 +            recover(
  47.165 +              reparse_spans(resources, syntax, get_blob, can_import, name, cmds, first, last))
  47.166 +          case None => cmds
  47.167 +        }
  47.168 +      recover(commands)
  47.169 +    }
  47.170 +
  47.171      edit match {
  47.172        case (_, Document.Node.Clear()) => node.clear
  47.173  
  47.174 @@ -276,8 +241,7 @@
  47.175          if (name.is_theory) {
  47.176            val commands0 = node.commands
  47.177            val commands1 = edit_text(text_edits, commands0)
  47.178 -          val commands2 =
  47.179 -            recover_spans(resources, syntax, get_blob, name, node.perspective.visible, commands1)
  47.180 +          val commands2 = recover_spans(name, node.perspective.visible, commands1)
  47.181            node.update_commands(commands2)
  47.182          }
  47.183          else node
  47.184 @@ -289,11 +253,33 @@
  47.185          val perspective: Document.Node.Perspective_Command =
  47.186            Document.Node.Perspective(required, visible_overlay, overlays)
  47.187          if (node.same_perspective(text_perspective, perspective)) node
  47.188 -        else
  47.189 -          node.update_perspective(text_perspective, perspective).
  47.190 -            update_commands(
  47.191 -              consolidate_spans(resources, syntax, get_blob, reparse_limit,
  47.192 -                name, visible, node.commands))
  47.193 +        else {
  47.194 +          /* consolidate unfinished spans */
  47.195 +          val is_visible = visible.commands.toSet
  47.196 +          val commands = node.commands
  47.197 +          val commands1 =
  47.198 +            if (is_visible.isEmpty) commands
  47.199 +            else {
  47.200 +              commands.find(_.is_unfinished) match {
  47.201 +                case Some(first_unfinished) =>
  47.202 +                  commands.reverse.find(is_visible) match {
  47.203 +                    case Some(last_visible) =>
  47.204 +                      val it = commands.iterator(last_visible)
  47.205 +                      var last = last_visible
  47.206 +                      var i = 0
  47.207 +                      while (i < reparse_limit && it.hasNext) {
  47.208 +                        last = it.next
  47.209 +                        i += last.length
  47.210 +                      }
  47.211 +                      reparse_spans(resources, syntax, get_blob, can_import,
  47.212 +                        name, commands, first_unfinished, last)
  47.213 +                    case None => commands
  47.214 +                  }
  47.215 +                case None => commands
  47.216 +              }
  47.217 +            }
  47.218 +          node.update_perspective(text_perspective, perspective).update_commands(commands1)
  47.219 +        }
  47.220      }
  47.221    }
  47.222  
  47.223 @@ -304,10 +290,13 @@
  47.224        doc_blobs: Document.Blobs,
  47.225        edits: List[Document.Edit_Text]): Session.Change =
  47.226    {
  47.227 +    val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
  47.228 +
  47.229      def get_blob(name: Document.Node.Name) =
  47.230        doc_blobs.get(name) orElse previous.nodes(name).get_blob
  47.231  
  47.232 -    val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
  47.233 +    def can_import(name: Document.Node.Name): Boolean =
  47.234 +      resources.loaded_theories(name.theory) || nodes0(name).has_header
  47.235  
  47.236      val (doc_edits, version) =
  47.237        if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
  47.238 @@ -337,14 +326,15 @@
  47.239              val node1 =
  47.240                if (reparse_set(name) && commands.nonEmpty)
  47.241                  node.update_commands(
  47.242 -                  reparse_spans(resources, syntax, get_blob,
  47.243 -                    name, commands, commands.head, commands.last))
  47.244 +                  reparse_spans(resources, syntax, get_blob, can_import, name,
  47.245 +                    commands, commands.head, commands.last))
  47.246                else node
  47.247              val node2 =
  47.248 -              (node1 /: edits)(text_edit(resources, syntax, get_blob, reparse_limit, _, _))
  47.249 +              (node1 /: edits)(
  47.250 +                text_edit(resources, syntax, get_blob, can_import, reparse_limit, _, _))
  47.251              val node3 =
  47.252                if (reparse_set.contains(name))
  47.253 -                text_edit(resources, syntax, get_blob, reparse_limit,
  47.254 +                text_edit(resources, syntax, get_blob, can_import, reparse_limit,
  47.255                    node2, (name, node2.edit_perspective))
  47.256                else node2
  47.257  
    48.1 --- a/src/Pure/Tools/build.scala	Mon Mar 16 15:30:00 2015 +0000
    48.2 +++ b/src/Pure/Tools/build.scala	Tue Mar 17 12:23:56 2015 +0000
    48.3 @@ -242,7 +242,7 @@
    48.4                { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
    48.5              rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
    48.6  
    48.7 -      command(SESSION) ~!
    48.8 +      position(command(SESSION)) ~!
    48.9          (session_name ~
   48.10            (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
   48.11            (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
   48.12 @@ -253,15 +253,16 @@
   48.13                rep1(theories) ~
   48.14                (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
   48.15                (rep(document_files) ^^ (x => x.flatten))))) ^^
   48.16 -        { case pos ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
   48.17 +        { case (_, pos) ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
   48.18              Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
   48.19      }
   48.20  
   48.21      def parse_entries(root: Path): List[(String, Session_Entry)] =
   48.22      {
   48.23        val toks = Token.explode(root_syntax.keywords, File.read(root))
   48.24 +      val start = Token.Pos.file(root.implode)
   48.25  
   48.26 -      parse_all(rep(chapter | session_entry), Token.reader(toks, root.implode)) match {
   48.27 +      parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
   48.28          case Success(result, _) =>
   48.29            var chapter = chapter_default
   48.30            val entries = new mutable.ListBuffer[(String, Session_Entry)]
    49.1 --- a/src/Pure/library.scala	Mon Mar 16 15:30:00 2015 +0000
    49.2 +++ b/src/Pure/library.scala	Tue Mar 17 12:23:56 2015 +0000
    49.3 @@ -16,9 +16,21 @@
    49.4  {
    49.5    /* user errors */
    49.6  
    49.7 +  class User_Error(message: String) extends RuntimeException(message)
    49.8 +  {
    49.9 +    override def equals(that: Any): Boolean =
   49.10 +      that match {
   49.11 +        case other: User_Error => message == other.getMessage
   49.12 +        case _ => false
   49.13 +      }
   49.14 +    override def hashCode: Int = message.hashCode
   49.15 +
   49.16 +    override def toString: String = "ERROR(" + message + ")"
   49.17 +  }
   49.18 +
   49.19    object ERROR
   49.20    {
   49.21 -    def apply(message: String): Throwable = new RuntimeException(message)
   49.22 +    def apply(message: String): User_Error = new User_Error(message)
   49.23      def unapply(exn: Throwable): Option[String] = Exn.user_message(exn)
   49.24    }
   49.25  
    50.1 --- a/src/Pure/raw_simplifier.ML	Mon Mar 16 15:30:00 2015 +0000
    50.2 +++ b/src/Pure/raw_simplifier.ML	Tue Mar 17 12:23:56 2015 +0000
    50.3 @@ -845,8 +845,15 @@
    50.4  fun check_conv ctxt msg thm thm' =
    50.5    let
    50.6      val thm'' = Thm.transitive thm thm' handle THM _ =>
    50.7 -     Thm.transitive thm (Thm.transitive
    50.8 -       (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
    50.9 +      let
   50.10 +        val nthm' =
   50.11 +          Thm.transitive (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm'
   50.12 +      in Thm.transitive thm nthm' handle THM _ =>
   50.13 +           let
   50.14 +             val nthm =
   50.15 +               Thm.transitive thm (Drule.beta_eta_conversion (Thm.rhs_of thm))
   50.16 +           in Thm.transitive nthm nthm' end
   50.17 +      end
   50.18      val _ =
   50.19        if msg then cond_tracing ctxt (fn () => print_thm ctxt "SUCCEEDED" ("", thm'))
   50.20        else ();
    51.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Mar 16 15:30:00 2015 +0000
    51.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Mar 17 12:23:56 2015 +0000
    51.3 @@ -79,7 +79,8 @@
    51.4      if (is_theory) {
    51.5        JEdit_Lib.buffer_lock(buffer) {
    51.6          Exn.capture {
    51.7 -          PIDE.resources.check_thy_reader("", node_name, JEdit_Lib.buffer_reader(buffer))
    51.8 +          PIDE.resources.check_thy_reader("", node_name,
    51.9 +            JEdit_Lib.buffer_reader(buffer), Token.Pos.file(node_name.node))
   51.10          } match {
   51.11            case Exn.Res(header) => header
   51.12            case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
    52.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Mar 16 15:30:00 2015 +0000
    52.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Mar 17 12:23:56 2015 +0000
    52.3 @@ -79,13 +79,6 @@
    52.4      }
    52.5    }
    52.6  
    52.7 -  def check_file(view: View, file: String): Boolean =
    52.8 -    try {
    52.9 -      if (Url.is_wellformed(file)) Url.is_readable(file)
   52.10 -      else (new JFile(file)).isFile
   52.11 -    }
   52.12 -    catch { case ERROR(_) => false }
   52.13 -
   52.14  
   52.15    /* file content */
   52.16  
    53.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Mar 16 15:30:00 2015 +0000
    53.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Mar 17 12:23:56 2015 +0000
    53.3 @@ -216,9 +216,8 @@
    53.4                } yield (model.node_name, Position.none)
    53.5  
    53.6              val thy_info = new Thy_Info(PIDE.resources)
    53.7 -            // FIXME avoid I/O on GUI thread!?!
    53.8              val files = thy_info.dependencies("", thys).deps.map(_.name.node).
    53.9 -              filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file))
   53.10 +              filter(file => !loaded_buffer(file) && PIDE.resources.check_file(file))
   53.11  
   53.12              if (files.nonEmpty) {
   53.13                if (PIDE.options.bool("jedit_auto_load")) {