--- a/src/HOL/Complex.thy Wed Mar 18 13:51:33 2015 +0100
+++ b/src/HOL/Complex.thy Wed Mar 18 14:28:40 2015 +0000
@@ -215,6 +215,18 @@
lemma i_even_power [simp]: "\<i> ^ (n * 2) = (-1) ^ n"
by (metis mult.commute power2_i power_mult)
+lemma Re_ii_times [simp]: "Re (ii*z) = - Im z"
+ by simp
+
+lemma Im_ii_times [simp]: "Im (ii*z) = Re z"
+ by simp
+
+lemma ii_times_eq_iff: "ii*w = z \<longleftrightarrow> w = -(ii*z)"
+ by auto
+
+lemma divide_numeral_i [simp]: "z / (numeral n * ii) = -(ii*z) / numeral n"
+ by (metis divide_divide_eq_left divide_i mult.commute mult_minus_right)
+
subsection {* Vector Norm *}
instantiation complex :: real_normed_field
@@ -309,6 +321,9 @@
apply (simp_all add: power2_sum add.commute sum_squares_bound real_sqrt_mult [symmetric])
done
+lemma complex_unit_circle: "z \<noteq> 0 \<Longrightarrow> (Re z / cmod z)\<^sup>2 + (Im z / cmod z)\<^sup>2 = 1"
+ by (simp add: norm_complex_def divide_simps complex_eq_iff)
+
text {* Properties of complex signum. *}
@@ -508,10 +523,10 @@
(auto simp: complex_eq_iff norm_complex_def power2_eq_square[symmetric] of_real_power[symmetric]
simp del: of_real_power)
-lemma re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
+lemma Re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
by (auto simp add: Re_divide)
-lemma im_complex_div_eq_0: "Im (a / b) = 0 \<longleftrightarrow> Im (a * cnj b) = 0"
+lemma Im_complex_div_eq_0: "Im (a / b) = 0 \<longleftrightarrow> Im (a * cnj b) = 0"
by (auto simp add: Im_divide)
lemma complex_div_gt_0:
@@ -526,27 +541,27 @@
by (simp add: Re_divide Im_divide zero_less_divide_iff)
qed
-lemma re_complex_div_gt_0: "Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0"
- and im_complex_div_gt_0: "Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0"
+lemma Re_complex_div_gt_0: "Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0"
+ and Im_complex_div_gt_0: "Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0"
using complex_div_gt_0 by auto
-lemma re_complex_div_ge_0: "Re(a / b) \<ge> 0 \<longleftrightarrow> Re(a * cnj b) \<ge> 0"
- by (metis le_less re_complex_div_eq_0 re_complex_div_gt_0)
+lemma Re_complex_div_ge_0: "Re(a / b) \<ge> 0 \<longleftrightarrow> Re(a * cnj b) \<ge> 0"
+ by (metis le_less Re_complex_div_eq_0 Re_complex_div_gt_0)
-lemma im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
- by (metis im_complex_div_eq_0 im_complex_div_gt_0 le_less)
+lemma Im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
+ by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 le_less)
-lemma re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
- by (metis less_asym neq_iff re_complex_div_eq_0 re_complex_div_gt_0)
+lemma Re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
+ by (metis less_asym neq_iff Re_complex_div_eq_0 Re_complex_div_gt_0)
-lemma im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
- by (metis im_complex_div_eq_0 im_complex_div_gt_0 less_asym neq_iff)
+lemma Im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
+ by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 less_asym neq_iff)
-lemma re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"
- by (metis not_le re_complex_div_gt_0)
+lemma Re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"
+ by (metis not_le Re_complex_div_gt_0)
-lemma im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
- by (metis im_complex_div_gt_0 not_le)
+lemma Im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
+ by (metis Im_complex_div_gt_0 not_le)
lemma Re_setsum[simp]: "Re (setsum f s) = (\<Sum>x\<in>s. Re (f x))"
by (induct s rule: infinite_finite_induct) auto
@@ -807,7 +822,7 @@
lemma csqrt_ii [simp]: "csqrt \<i> = (1 + \<i>) / sqrt 2"
by (simp add: complex_eq_iff Re_divide Im_divide real_sqrt_divide real_div_sqrt)
-lemma power2_csqrt[algebra]: "(csqrt z)\<^sup>2 = z"
+lemma power2_csqrt[simp,algebra]: "(csqrt z)\<^sup>2 = z"
proof cases
assume "Im z = 0" then show ?thesis
using real_sqrt_pow2[of "Re z"] real_sqrt_pow2[of "- Re z"]
--- a/src/HOL/Decision_Procs/Approximation.thy Wed Mar 18 13:51:33 2015 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Mar 18 14:28:40 2015 +0000
@@ -1718,8 +1718,10 @@
by (auto simp: real_power_down_fl intro!: power_down_le)
next
case True
- have "power_down_fl prec (Float 1 (- 2)) ?num \<le> real (Float 1 (- 2)) ^ ?num"
- by (auto simp: real_power_down_fl power_down)
+ have "power_down_fl prec (Float 1 (- 2)) ?num \<le> (Float 1 (- 2)) ^ ?num"
+ by (metis Float_le_zero_iff less_imp_le linorder_not_less not_numeral_le_zero numeral_One power_down_fl)
+ then have "power_down_fl prec (Float 1 (- 2)) ?num \<le> real (Float 1 (- 2)) ^ ?num"
+ by simp
also
have "real (floor_fl x) \<noteq> 0" and "real (floor_fl x) \<le> 0" using `real (floor_fl x) < 0` by auto
from divide_right_mono_neg[OF floor_fl[of x] `real (floor_fl x) \<le> 0`, unfolded divide_self[OF `real (floor_fl x) \<noteq> 0`]]
@@ -1727,7 +1729,7 @@
from order_trans[OF exp_m1_ge_quarter this[unfolded exp_le_cancel_iff[where x="- 1", symmetric]]]
have "Float 1 (- 2) \<le> exp (x / (- floor_fl x))" unfolding Float_num .
hence "real (Float 1 (- 2)) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
- by (auto intro!: power_mono)
+ by (metis Float_num(5) power_mono zero_le_divide_1_iff zero_le_numeral)
also have "\<dots> = exp x" unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric] using `real (floor_fl x) \<noteq> 0` by auto
finally show ?thesis
unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] if_P[OF `x < - 1`] int_floor_fl_def Let_def if_P[OF True] real_of_float_power
--- a/src/HOL/Library/Formal_Power_Series.thy Wed Mar 18 13:51:33 2015 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Wed Mar 18 14:28:40 2015 +0000
@@ -8,8 +8,6 @@
imports Complex_Main
begin
-lemmas fact_Suc = fact.simps(2)
-
subsection {* The type of formal power series*}
typedef 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
@@ -594,7 +592,7 @@
fix n :: nat
assume nn0: "n \<ge> n0"
then have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0"
- by (auto intro: power_decreasing)
+ by (simp add: divide_simps)
{
assume "?s n = a"
then have "dist (?s n) a < r"
@@ -612,9 +610,9 @@
by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff
split: split_if_asm intro: LeastI2_ex)
then have "dist (?s n) a < (1/2)^n"
- unfolding dth by (auto intro: power_strict_decreasing)
+ unfolding dth by (simp add: divide_simps)
also have "\<dots> \<le> (1/2)^n0"
- using nn0 by (auto intro: power_decreasing)
+ using nn0 by (simp add: divide_simps)
also have "\<dots> < r"
using n0 by simp
finally have "dist (?s n) a < r" .
--- a/src/HOL/NthRoot.thy Wed Mar 18 13:51:33 2015 +0100
+++ b/src/HOL/NthRoot.thy Wed Mar 18 14:28:40 2015 +0000
@@ -626,19 +626,24 @@
apply (simp add: zero_less_divide_iff)
done
+lemma sqrt2_less_2: "sqrt 2 < (2::real)"
+ by (metis not_less not_less_iff_gr_or_eq numeral_less_iff real_sqrt_four real_sqrt_le_iff semiring_norm(75) semiring_norm(78) semiring_norm(85))
+
+
text{*Needed for the infinitely close relation over the nonstandard
complex numbers*}
lemma lemma_sqrt_hcomplex_capprox:
"[| 0 < u; x < u/2; y < u/2; 0 \<le> x; 0 \<le> y |] ==> sqrt (x\<^sup>2 + y\<^sup>2) < u"
-apply (rule_tac y = "u/sqrt 2" in order_le_less_trans)
-apply (erule_tac [2] lemma_real_divide_sqrt_less)
-apply (rule power2_le_imp_le)
-apply (auto simp add: zero_le_divide_iff power_divide)
-apply (rule_tac t = "u\<^sup>2" in real_sum_of_halves [THEN subst])
-apply (rule add_mono)
-apply (auto simp add: four_x_squared intro: power_mono)
-done
-
+ apply (rule real_sqrt_sum_squares_less)
+ apply (auto simp add: abs_if field_simps)
+ apply (rule le_less_trans [where y = "x*2"])
+ using less_eq_real_def sqrt2_less_2 apply force
+ apply assumption
+ apply (rule le_less_trans [where y = "y*2"])
+ using less_eq_real_def sqrt2_less_2 mult_le_cancel_left
+ apply auto
+ done
+
text "Legacy theorem names:"
lemmas real_root_pos2 = real_root_power_cancel
lemmas real_root_pos_pos = real_root_gt_zero [THEN order_less_imp_le]
--- a/src/HOL/Power.thy Wed Mar 18 13:51:33 2015 +0100
+++ b/src/HOL/Power.thy Wed Mar 18 14:28:40 2015 +0000
@@ -51,6 +51,10 @@
"a ^ 1 = a"
by simp
+lemma power_Suc0_right [simp]:
+ "a ^ Suc 0 = a"
+ by simp
+
lemma power_commutes:
"a ^ n * a = a * a ^ n"
by (induct n) (simp_all add: mult.assoc)
@@ -127,6 +131,9 @@
end
+declare power_mult_distrib [where a = "numeral w" for w, simp]
+declare power_mult_distrib [where b = "numeral w" for w, simp]
+
context semiring_numeral
begin
@@ -301,6 +308,8 @@
"b \<noteq> 0 \<Longrightarrow> (a / b) ^ n = a ^ n / b ^ n"
by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
+declare nonzero_power_divide [where b = "numeral w" for w, simp]
+
end
--- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Mar 18 13:51:33 2015 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Mar 18 14:28:40 2015 +0000
@@ -502,13 +502,26 @@
end
lemma emeasure_lborel_UNIV: "emeasure lborel (UNIV::'a::euclidean_space set) = \<infinity>"
- unfolding UN_box_eq_UNIV[symmetric]
- apply (subst SUP_emeasure_incseq[symmetric])
- apply (auto simp: incseq_def subset_box inner_add_left setprod_constant intro!: SUP_PInfty)
- apply (rule_tac x="Suc n" in exI)
- apply (rule order_trans[OF _ self_le_power])
- apply (auto simp: card_gt_0_iff real_of_nat_Suc)
- done
+proof -
+ { fix n::nat
+ let ?Ba = "Basis :: 'a set"
+ have "real n \<le> (2::real) ^ card ?Ba * real n"
+ by (simp add: mult_le_cancel_right1)
+ also
+ have "... \<le> (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba"
+ apply (rule mult_left_mono)
+ apply (metis DIM_positive One_nat_def less_eq_Suc_le less_imp_le real_of_nat_le_iff real_of_nat_power self_le_power zero_less_Suc)
+ apply (simp add: DIM_positive)
+ done
+ finally have "real n \<le> (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba" .
+ } note [intro!] = this
+ show ?thesis
+ unfolding UN_box_eq_UNIV[symmetric]
+ apply (subst SUP_emeasure_incseq[symmetric])
+ apply (auto simp: incseq_def subset_box inner_add_left setprod_constant
+ intro!: SUP_PInfty)
+ done
+qed
lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0"
using emeasure_lborel_cbox[of x x] nonempty_Basis
--- a/src/HOL/ROOT Wed Mar 18 13:51:33 2015 +0100
+++ b/src/HOL/ROOT Wed Mar 18 14:28:40 2015 +0000
@@ -689,6 +689,7 @@
Determinants
PolyRoots
Complex_Analysis_Basics
+ Complex_Transcendental
document_files
"root.tex"
--- a/src/HOL/Real_Vector_Spaces.thy Wed Mar 18 13:51:33 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Wed Mar 18 14:28:40 2015 +0000
@@ -444,7 +444,8 @@
then show thesis ..
qed
-lemma setsum_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setsum f s \<in> \<real>"
+lemma setsum_in_Reals [intro,simp]:
+ assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setsum f s \<in> \<real>"
proof (cases "finite s")
case True then show ?thesis using assms
by (induct s rule: finite_induct) auto
@@ -453,7 +454,8 @@
by (metis Reals_0 setsum.infinite)
qed
-lemma setprod_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
+lemma setprod_in_Reals [intro,simp]:
+ assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
proof (cases "finite s")
case True then show ?thesis using assms
by (induct s rule: finite_induct) auto
--- a/src/HOL/Series.thy Wed Mar 18 13:51:33 2015 +0100
+++ b/src/HOL/Series.thy Wed Mar 18 14:28:40 2015 +0000
@@ -434,7 +434,7 @@
have 2: "(\<lambda>n. (1/2::real)^n) sums 2" using geometric_sums [of "1/2::real"]
by auto
have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)"
- by simp
+ by (simp add: mult.commute)
thus ?thesis using sums_divide [OF 2, of 2]
by simp
qed
--- a/src/HOL/Transcendental.thy Wed Mar 18 13:51:33 2015 +0100
+++ b/src/HOL/Transcendental.thy Wed Mar 18 14:28:40 2015 +0000
@@ -1512,6 +1512,10 @@
using exp_bound [of "1/2"]
by (simp add: field_simps)
+corollary exp_le: "exp 1 \<le> (3::real)"
+ using exp_bound [of 1]
+ by (simp add: field_simps)
+
lemma exp_bound_half: "norm(z) \<le> 1/2 \<Longrightarrow> norm(exp z) \<le> 2"
by (blast intro: order_trans intro!: exp_half_le2 norm_exp)
@@ -3071,6 +3075,84 @@
lemma sin_two_pi [simp]: "sin (2*pi) = 0"
by (simp add: sin_double)
+
+lemma sin_times_sin:
+ fixes w :: "'a::{real_normed_field,banach}"
+ shows "sin(w) * sin(z) = (cos(w - z) - cos(w + z)) / 2"
+ by (simp add: cos_diff cos_add)
+
+lemma sin_times_cos:
+ fixes w :: "'a::{real_normed_field,banach}"
+ shows "sin(w) * cos(z) = (sin(w + z) + sin(w - z)) / 2"
+ by (simp add: sin_diff sin_add)
+
+lemma cos_times_sin:
+ fixes w :: "'a::{real_normed_field,banach}"
+ shows "cos(w) * sin(z) = (sin(w + z) - sin(w - z)) / 2"
+ by (simp add: sin_diff sin_add)
+
+lemma cos_times_cos:
+ fixes w :: "'a::{real_normed_field,banach}"
+ shows "cos(w) * cos(z) = (cos(w - z) + cos(w + z)) / 2"
+ by (simp add: cos_diff cos_add)
+
+lemma sin_plus_sin: (*FIXME field_inverse_zero should not be necessary*)
+ fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
+ shows "sin(w) + sin(z) = 2 * sin((w + z) / 2) * cos((w - z) / 2)"
+ apply (simp add: mult.assoc sin_times_cos)
+ apply (simp add: field_simps)
+ done
+
+lemma sin_diff_sin:
+ fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
+ shows "sin(w) - sin(z) = 2 * sin((w - z) / 2) * cos((w + z) / 2)"
+ apply (simp add: mult.assoc sin_times_cos)
+ apply (simp add: field_simps)
+ done
+
+lemma cos_plus_cos:
+ fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
+ shows "cos(w) + cos(z) = 2 * cos((w + z) / 2) * cos((w - z) / 2)"
+ apply (simp add: mult.assoc cos_times_cos)
+ apply (simp add: field_simps)
+ done
+
+lemma cos_diff_cos:
+ fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
+ shows "cos(w) - cos(z) = 2 * sin((w + z) / 2) * sin((z - w) / 2)"
+ apply (simp add: mult.assoc sin_times_sin)
+ apply (simp add: field_simps)
+ done
+
+lemma cos_double_cos:
+ fixes z :: "'a::{real_normed_field,banach}"
+ shows "cos(2 * z) = 2 * cos z ^ 2 - 1"
+by (simp add: cos_double sin_squared_eq)
+
+lemma cos_double_sin:
+ fixes z :: "'a::{real_normed_field,banach}"
+ shows "cos(2 * z) = 1 - 2 * sin z ^ 2"
+by (simp add: cos_double sin_squared_eq)
+
+lemma sin_pi_minus [simp]: "sin (pi - x) = sin x"
+ by (metis sin_minus sin_periodic_pi minus_minus uminus_add_conv_diff)
+
+lemma cos_pi_minus [simp]: "cos (pi - x) = -(cos x)"
+ by (metis cos_minus cos_periodic_pi uminus_add_conv_diff)
+
+lemma sin_minus_pi [simp]: "sin (x - pi) = - (sin x)"
+ by (simp add: sin_diff)
+
+lemma cos_minus_pi [simp]: "cos (x - pi) = -(cos x)"
+ by (simp add: cos_diff)
+
+lemma sin_2pi_minus [simp]: "sin (2*pi - x) = -(sin x)"
+ by (metis sin_periodic_pi2 add_diff_eq mult_2 sin_pi_minus)
+
+lemma cos_2pi_minus [simp]: "cos (2*pi - x) = cos x"
+ by (metis (no_types, hide_lams) cos_add cos_minus cos_two_pi sin_minus sin_two_pi
+ diff_0_right minus_diff_eq mult_1 mult_zero_left uminus_add_conv_diff)
+
lemma sin_gt_zero2: "\<lbrakk>0 < x; x < pi/2\<rbrakk> \<Longrightarrow> 0 < sin x"
by (metis sin_gt_zero_02 order_less_trans pi_half_less_two)
--- a/src/Pure/Isar/keyword.ML Wed Mar 18 13:51:33 2015 +0100
+++ b/src/Pure/Isar/keyword.ML Wed Mar 18 14:28:40 2015 +0000
@@ -50,7 +50,6 @@
val is_document_body: keywords -> string -> bool
val is_document_raw: keywords -> string -> bool
val is_document: keywords -> string -> bool
- val is_theory_begin: keywords -> string -> bool
val is_theory_end: keywords -> string -> bool
val is_theory_load: keywords -> string -> bool
val is_theory: keywords -> string -> bool
@@ -219,7 +218,6 @@
val is_document_raw = command_category [document_raw];
val is_document = command_category [document_heading, document_body, document_raw];
-val is_theory_begin = command_category [thy_begin];
val is_theory_end = command_category [thy_end];
val is_theory_load = command_category [thy_load];
--- a/src/Pure/Isar/outer_syntax.scala Wed Mar 18 13:51:33 2015 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Wed Mar 18 14:28:40 2015 +0000
@@ -123,9 +123,7 @@
}
- /* command categories */
-
- def is_theory_begin(name: String): Boolean = keywords.is_command_kind(name, Keyword.theory_begin)
+ /* load commands */
def load_command(name: String): Option[List[String]] = keywords.load_command(name)
def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
@@ -230,13 +228,14 @@
def heading_level(command: Command): Option[Int] =
{
- command.name match {
- case "chapter" => Some(0)
- case "section" | "header" => Some(1)
- case "subsection" => Some(2)
- case "subsubsection" => Some(3)
+ val name = command.span.name
+ name match {
+ case Thy_Header.CHAPTER => Some(0)
+ case Thy_Header.SECTION | Thy_Header.HEADER => Some(1)
+ case Thy_Header.SUBSECTION => Some(2)
+ case Thy_Header.SUBSUBSECTION => Some(3)
case _ =>
- keywords.command_kind(command.name) match {
+ keywords.command_kind(name) match {
case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(4)
case _ => None
}
@@ -258,7 +257,7 @@
{
stack match {
case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
- body2 += Outer_Syntax.Document_Block(command.name, command.source, body.toList)
+ body2 += Outer_Syntax.Document_Block(command.span.name, command.source, body.toList)
stack = stack.tail
close(level)
case _ =>
--- a/src/Pure/Isar/token.scala Wed Mar 18 13:51:33 2015 +0100
+++ b/src/Pure/Isar/token.scala Wed Mar 18 14:28:40 2015 +0000
@@ -153,6 +153,15 @@
}
+ /* implode */
+
+ def implode(toks: List[Token]): String =
+ toks match {
+ case List(tok) => tok.source
+ case toks => toks.map(_.source).mkString
+ }
+
+
/* token reader */
object Pos
--- a/src/Pure/PIDE/command.scala Wed Mar 18 13:51:33 2015 +0100
+++ b/src/Pure/PIDE/command.scala Wed Mar 18 14:28:40 2015 +0000
@@ -235,7 +235,7 @@
for {
(chunk_name, chunk) <- command.chunks.iterator
range <- Protocol_Message.positions(
- self_id, command.position, chunk_name, chunk, message)
+ self_id, command.span.position, chunk_name, chunk, message)
} st = st.add_markup(false, chunk_name, Text.Info(range, message2))
}
st
@@ -334,19 +334,15 @@
}
def span_files(syntax: Prover.Syntax, span: Command_Span.Span): (List[String], Int) =
- span.kind match {
- case Command_Span.Command_Span(name, _) =>
- syntax.load_command(name) match {
- case Some(exts) =>
- find_file(clean_tokens(span.content)) match {
- case Some((file, i)) =>
- if (exts.isEmpty) (List(file), i)
- else (exts.map(ext => file + "." + ext), i)
- case None => (Nil, -1)
- }
+ syntax.load_command(span.name) match {
+ case Some(exts) =>
+ find_file(clean_tokens(span.content)) match {
+ case Some((file, i)) =>
+ if (exts.isEmpty) (List(file), i)
+ else (exts.map(ext => file + "." + ext), i)
case None => (Nil, -1)
}
- case _ => (Nil, -1)
+ case None => (Nil, -1)
}
def blobs_info(
@@ -357,12 +353,12 @@
node_name: Document.Node.Name,
span: Command_Span.Span): Blobs_Info =
{
- span.kind match {
+ span.name match {
// inlined errors
- case Command_Span.Command_Span(name, _) if syntax.is_theory_begin(name) =>
+ case Thy_Header.THEORY =>
val header =
resources.check_thy_reader("", node_name,
- new CharSequenceReader(span.source), Token.Pos.command)
+ new CharSequenceReader(Token.implode(span.content)), Token.Pos.command)
val errors =
for ((imp, pos) <- header.imports if !can_import(imp)) yield {
val msg =
@@ -398,14 +394,6 @@
val init_results: Command.Results,
val init_markup: Markup_Tree)
{
- /* name */
-
- def name: String =
- span.kind match { case Command_Span.Command_Span(name, _) => name case _ => "" }
-
- def position: Position.T =
- span.kind match { case Command_Span.Command_Span(_, pos) => pos case _ => Position.none }
-
override def toString: String = id + "/" + span.kind.toString
--- a/src/Pure/PIDE/command_span.scala Wed Mar 18 13:51:33 2015 +0100
+++ b/src/Pure/PIDE/command_span.scala Wed Mar 18 14:28:40 2015 +0000
@@ -26,26 +26,26 @@
sealed case class Span(kind: Kind, content: List[Token])
{
- def length: Int = (0 /: content)(_ + _.source.length)
+ def name: String =
+ kind match { case Command_Span(name, _) => name case _ => "" }
- def source: String =
- content match {
- case List(tok) => tok.source
- case toks => toks.map(_.source).mkString
- }
+ def position: Position.T =
+ kind match { case Command_Span(_, pos) => pos case _ => Position.none }
+
+ def length: Int = (0 /: content)(_ + _.source.length)
def compact_source: (String, Span) =
{
- val src = source
+ val source = Token.implode(content)
val content1 = new mutable.ListBuffer[Token]
var i = 0
for (Token(kind, s) <- content) {
val n = s.length
- val s1 = src.substring(i, i + n)
+ val s1 = source.substring(i, i + n)
content1 += Token(kind, s1)
i += n
}
- (src, Span(kind, content1.toList))
+ (source, Span(kind, content1.toList))
}
}
--- a/src/Pure/PIDE/document.ML Wed Mar 18 13:51:33 2015 +0100
+++ b/src/Pure/PIDE/document.ML Wed Mar 18 14:28:40 2015 +0000
@@ -552,8 +552,7 @@
val initial' = initial andalso
(case prev of
NONE => true
- | SOME command_id =>
- not (Keyword.is_theory_begin keywords (the_command_name state command_id)));
+ | SOME command_id => the_command_name state command_id <> Thy_Header.theoryN);
in (visible', initial') end;
fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) =
@@ -614,7 +613,7 @@
val exec' = (eval', prints');
val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
- val init' = if Keyword.is_theory_begin keywords command_name then NONE else init;
+ val init' = if command_name = Thy_Header.theoryN then NONE else init;
in SOME (assign_update', (command_id', (eval', prints')), init') end;
fun removed_execs node0 (command_id, exec_ids) =
--- a/src/Pure/PIDE/protocol.scala Wed Mar 18 13:51:33 2015 +0100
+++ b/src/Pure/PIDE/protocol.scala Wed Mar 18 14:28:40 2015 +0000
@@ -329,7 +329,7 @@
}
protocol_command("Document.define_command",
- (Document_ID(command.id) :: encode(command.name) :: blobs_yxml :: toks_yxml ::
+ (Document_ID(command.id) :: encode(command.span.name) :: blobs_yxml :: toks_yxml ::
toks.map(tok => encode(tok.source))): _*)
}
--- a/src/Pure/PIDE/prover.scala Wed Mar 18 13:51:33 2015 +0100
+++ b/src/Pure/PIDE/prover.scala Wed Mar 18 14:28:40 2015 +0000
@@ -20,7 +20,6 @@
def ++ (other: Syntax): Syntax
def add_keywords(keywords: Thy_Header.Keywords): Syntax
def parse_spans(input: CharSequence): List[Command_Span.Span]
- def is_theory_begin(name: String): Boolean
def load_command(name: String): Option[List[String]]
def load_commands_in(text: String): Boolean
}
--- a/src/Pure/Thy/thy_header.ML Wed Mar 18 13:51:33 2015 +0100
+++ b/src/Pure/Thy/thy_header.ML Wed Mar 18 14:28:40 2015 +0000
@@ -12,6 +12,7 @@
imports: (string * Position.T) list,
keywords: keywords}
val make: string * Position.T -> (string * Position.T) list -> keywords -> header
+ val theoryN: string
val bootstrap_keywords: Keyword.keywords
val add_keywords: keywords -> theory -> theory
val get_keywords: theory -> Keyword.keywords
--- a/src/Pure/Thy/thy_header.scala Wed Mar 18 13:51:33 2015 +0100
+++ b/src/Pure/Thy/thy_header.scala Wed Mar 18 14:28:40 2015 +0000
@@ -60,7 +60,7 @@
private val bootstrap_keywords =
Keyword.Keywords.empty.add_keywords(bootstrap_header)
- def bootstrap_syntax(): Outer_Syntax =
+ lazy val bootstrap_syntax: Outer_Syntax =
Outer_Syntax.init().add_keywords(bootstrap_header)
--- a/src/Pure/Tools/build.scala Wed Mar 18 13:51:33 2015 +0100
+++ b/src/Pure/Tools/build.scala Wed Mar 18 14:28:40 2015 +0000
@@ -438,7 +438,7 @@
info.parent.map(deps(_)) match {
case None =>
(Set.empty[String], Map.empty[String, Document.Node.Name],
- Thy_Header.bootstrap_syntax())
+ Thy_Header.bootstrap_syntax)
case Some(parent) =>
(parent.loaded_theories, parent.known_theories, parent.syntax)
}
--- a/src/Tools/jEdit/src/document_model.scala Wed Mar 18 13:51:33 2015 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Wed Mar 18 14:28:40 2015 +0000
@@ -12,6 +12,7 @@
import isabelle._
import scala.collection.mutable
+import scala.util.parsing.input.CharSequenceReader
import org.gjt.sp.jedit.jEdit
import org.gjt.sp.jedit.Buffer
@@ -78,13 +79,19 @@
if (is_theory) {
JEdit_Lib.buffer_lock(buffer) {
- Exn.capture {
- PIDE.resources.check_thy_reader("", node_name,
- JEdit_Lib.buffer_reader(buffer), Token.Pos.command)
- } match {
- case Exn.Res(header) => header
- case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
- }
+ Token_Markup.line_token_iterator(
+ Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst(
+ {
+ case Text.Info(range, tok)
+ if tok.is_command && tok.source == Thy_Header.THEORY => range.start
+ })
+ match {
+ case Some(offset) =>
+ val length = buffer.getLength - offset
+ PIDE.resources.check_thy_reader("", node_name,
+ new CharSequenceReader(buffer.getSegment(offset, length)), Token.Pos.command)
+ case None => Document.Node.no_header
+ }
}
}
else Document.Node.no_header
--- a/src/Tools/jEdit/src/timing_dockable.scala Wed Mar 18 13:51:33 2015 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala Wed Mar 18 14:28:40 2015 +0000
@@ -86,13 +86,15 @@
private case class Theory_Entry(name: Document.Node.Name, timing: Double, current: Boolean)
extends Entry
{
- def print: String = Time.print_seconds(timing) + "s theory " + quote(name.theory)
+ def print: String =
+ Time.print_seconds(timing) + "s theory " + quote(name.theory)
def follow(snapshot: Document.Snapshot) { PIDE.editor.goto_file(view, name.node) }
}
private case class Command_Entry(command: Command, timing: Double) extends Entry
{
- def print: String = " " + Time.print_seconds(timing) + "s command " + quote(command.name)
+ def print: String =
+ " " + Time.print_seconds(timing) + "s command " + quote(command.span.name)
def follow(snapshot: Document.Snapshot)
{ PIDE.editor.hyperlink_command(snapshot, command).foreach(_.follow(view)) }
}