--- a/NEWS Mon Sep 05 19:18:38 2011 +0200
+++ b/NEWS Tue Sep 06 07:23:45 2011 +0200
@@ -277,6 +277,8 @@
realpow_two_diff ~> square_diff_square_factored
reals_complete2 ~> complete_real
exp_ln_eq ~> ln_unique
+ expi_add ~> exp_add
+ expi_zero ~> exp_zero
lemma_DERIV_subst ~> DERIV_cong
LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff
LIMSEQ_const ~> tendsto_const
@@ -296,6 +298,9 @@
LIMSEQ_norm_zero ~> tendsto_norm_zero_iff
LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff
LIMSEQ_imp_rabs ~> tendsto_rabs
+ LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus]
+ LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const]
+ LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const]
LIM_ident ~> tendsto_ident_at
LIM_const ~> tendsto_const
LIM_add ~> tendsto_add
--- a/etc/isabelle.css Mon Sep 05 19:18:38 2011 +0200
+++ b/etc/isabelle.css Tue Sep 06 07:23:45 2011 +0200
@@ -40,7 +40,6 @@
.keyword { font-weight: bold; }
.operator { }
.command { font-weight: bold; }
-.ident { }
.string { color: #008B00; }
.altstring { color: #8B8B00; }
.verbatim { color: #00008B; }
--- a/src/HOL/Complex.thy Mon Sep 05 19:18:38 2011 +0200
+++ b/src/HOL/Complex.thy Tue Sep 06 07:23:45 2011 +0200
@@ -592,21 +592,20 @@
subsection{*Finally! Polar Form for Complex Numbers*}
-definition
+text {* An abbreviation for @{text "cos a + i sin a"}. *}
- (* abbreviation for (cos a + i sin a) *)
- cis :: "real => complex" where
+definition cis :: "real \<Rightarrow> complex" where
"cis a = Complex (cos a) (sin a)"
-definition
- (* abbreviation for r*(cos a + i sin a) *)
- rcis :: "[real, real] => complex" where
+text {* An abbreviation for @{text "r(cos a + i sin a)"}. *}
+
+definition rcis :: "[real, real] \<Rightarrow> complex" where
"rcis r a = complex_of_real r * cis a"
abbreviation expi :: "complex \<Rightarrow> complex"
where "expi \<equiv> exp"
-lemma expi_imaginary: "expi (Complex 0 b) = cis b"
+lemma cis_conv_exp: "cis b = exp (Complex 0 b)"
proof (rule complex_eqI)
{ fix n have "Complex 0 b ^ n =
real (fact n) *\<^sub>R Complex (cos_coeff n * b ^ n) (sin_coeff n * b ^ n)"
@@ -614,23 +613,18 @@
apply (simp add: cos_coeff_def sin_coeff_def)
apply (simp add: sin_coeff_Suc cos_coeff_Suc del: mult_Suc)
done } note * = this
- show "Re (exp (Complex 0 b)) = Re (cis b)"
+ show "Re (cis b) = Re (exp (Complex 0 b))"
unfolding exp_def cis_def cos_def
by (subst bounded_linear.suminf[OF bounded_linear_Re summable_exp_generic],
simp add: * mult_assoc [symmetric])
- show "Im (exp (Complex 0 b)) = Im (cis b)"
+ show "Im (cis b) = Im (exp (Complex 0 b))"
unfolding exp_def cis_def sin_def
by (subst bounded_linear.suminf[OF bounded_linear_Im summable_exp_generic],
simp add: * mult_assoc [symmetric])
qed
lemma expi_def: "expi z = complex_of_real (exp (Re z)) * cis (Im z)"
-proof -
- have "expi z = expi (complex_of_real (Re z) + Complex 0 (Im z))"
- by simp
- thus ?thesis
- unfolding exp_add exp_of_real expi_imaginary .
-qed
+ unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by simp
lemma complex_split_polar:
"\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
@@ -665,11 +659,6 @@
lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
by simp
-
-(*---------------------------------------------------------------------------*)
-(* (r1 * cis a) * (r2 * cis b) = r1 * r2 * cis (a + b) *)
-(*---------------------------------------------------------------------------*)
-
lemma cis_rcis_eq: "cis a = rcis 1 a"
by (simp add: rcis_def)
@@ -736,12 +725,6 @@
lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
by (auto simp add: DeMoivre)
-lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
- by (rule exp_add) (* FIXME: redundant *)
-
-lemma expi_zero: "expi (0::complex) = 1"
- by (rule exp_zero) (* FIXME: redundant *)
-
lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
apply (insert rcis_Ex [of z])
apply (auto simp add: expi_def rcis_def mult_assoc [symmetric])
--- a/src/HOL/Int.thy Mon Sep 05 19:18:38 2011 +0200
+++ b/src/HOL/Int.thy Tue Sep 06 07:23:45 2011 +0200
@@ -162,7 +162,10 @@
by (simp add: Zero_int_def One_int_def)
qed
-lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
+abbreviation int :: "nat \<Rightarrow> int" where
+ "int \<equiv> of_nat"
+
+lemma int_def: "int m = Abs_Integ (intrel `` {(m, 0)})"
by (induct m) (simp_all add: Zero_int_def One_int_def add)
@@ -218,7 +221,7 @@
text{*strict, in 1st argument; proof is by induction on k>0*}
lemma zmult_zless_mono2_lemma:
- "(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j"
+ "(i::int)<j ==> 0<k ==> int k * i < int k * j"
apply (induct k)
apply simp
apply (simp add: left_distrib)
@@ -226,13 +229,13 @@
apply (simp_all add: add_strict_mono)
done
-lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
+lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = int n"
apply (cases k)
apply (auto simp add: le add int_def Zero_int_def)
apply (rule_tac x="x-y" in exI, simp)
done
-lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
+lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = int n"
apply (cases k)
apply (simp add: less int_def Zero_int_def)
apply (rule_tac x="x-y" in exI, simp)
@@ -261,7 +264,7 @@
done
lemma zless_iff_Suc_zadd:
- "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + of_nat (Suc n))"
+ "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
apply (cases z, cases w)
apply (auto simp add: less add int_def)
apply (rename_tac a b c d)
@@ -314,7 +317,7 @@
done
text{*Collapse nested embeddings*}
-lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
+lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
by (induct n) auto
lemma of_int_power:
@@ -400,13 +403,13 @@
by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
qed
-lemma nat_int [simp]: "nat (of_nat n) = n"
+lemma nat_int [simp]: "nat (int n) = n"
by (simp add: nat int_def)
-lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)"
+lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
by (cases z) (simp add: nat le int_def Zero_int_def)
-corollary nat_0_le: "0 \<le> z ==> of_nat (nat z) = z"
+corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
by simp
lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
@@ -431,14 +434,14 @@
lemma nonneg_eq_int:
fixes z :: int
- assumes "0 \<le> z" and "\<And>m. z = of_nat m \<Longrightarrow> P"
+ assumes "0 \<le> z" and "\<And>m. z = int m \<Longrightarrow> P"
shows P
using assms by (blast dest: nat_0_le sym)
-lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)"
+lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
by (cases w) (simp add: nat le int_def Zero_int_def, arith)
-corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)"
+corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
by (simp only: eq_commute [of m] nat_eq_iff)
lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
@@ -446,7 +449,7 @@
apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith)
done
-lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> of_nat n"
+lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
by (cases x, simp add: nat le int_def le_diff_conv)
lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
@@ -470,10 +473,10 @@
by (cases z, cases z')
(simp add: nat add minus diff_minus le Zero_int_def)
-lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0"
+lemma nat_zminus_int [simp]: "nat (- int n) = 0"
by (simp add: int_def minus nat Zero_int_def)
-lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)"
+lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
by (cases z) (simp add: nat less int_def, arith)
context ring_1
@@ -491,31 +494,31 @@
subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
-lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \<Colon> int)"
+lemma negative_zless_0: "- (int (Suc n)) < (0 \<Colon> int)"
by (simp add: order_less_le del: of_nat_Suc)
-lemma negative_zless [iff]: "- (of_nat (Suc n)) < (of_nat m \<Colon> int)"
+lemma negative_zless [iff]: "- (int (Suc n)) < int m"
by (rule negative_zless_0 [THEN order_less_le_trans], simp)
-lemma negative_zle_0: "- of_nat n \<le> (0 \<Colon> int)"
+lemma negative_zle_0: "- int n \<le> 0"
by (simp add: minus_le_iff)
-lemma negative_zle [iff]: "- of_nat n \<le> (of_nat m \<Colon> int)"
+lemma negative_zle [iff]: "- int n \<le> int m"
by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
-lemma not_zle_0_negative [simp]: "~ (0 \<le> - (of_nat (Suc n) \<Colon> int))"
+lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
by (subst le_minus_iff, simp del: of_nat_Suc)
-lemma int_zle_neg: "((of_nat n \<Colon> int) \<le> - of_nat m) = (n = 0 & m = 0)"
+lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
by (simp add: int_def le minus Zero_int_def)
-lemma not_int_zless_negative [simp]: "~ ((of_nat n \<Colon> int) < - of_nat m)"
+lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
by (simp add: linorder_not_less)
-lemma negative_eq_positive [simp]: "((- of_nat n \<Colon> int) = of_nat m) = (n = 0 & m = 0)"
+lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)"
by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
-lemma zle_iff_zadd: "(w\<Colon>int) \<le> z \<longleftrightarrow> (\<exists>n. z = w + of_nat n)"
+lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)"
proof -
have "(w \<le> z) = (0 \<le> z - w)"
by (simp only: le_diff_eq add_0_left)
@@ -526,10 +529,10 @@
finally show ?thesis .
qed
-lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\<Colon>int)"
+lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
by simp
-lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\<Colon>int)"
+lemma int_Suc0_eq_1: "int (Suc 0) = 1"
by simp
text{*This version is proved for all ordered rings, not just integers!
@@ -540,7 +543,7 @@
"P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
-lemma negD: "(x \<Colon> int) < 0 \<Longrightarrow> \<exists>n. x = - (of_nat (Suc n))"
+lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
apply (cases x)
apply (auto simp add: le minus Zero_int_def int_def order_less_le)
apply (rule_tac x="y - Suc x" in exI, arith)
@@ -553,7 +556,7 @@
whether an integer is negative or not.*}
theorem int_cases [case_names nonneg neg, cases type: int]:
- "[|!! n. (z \<Colon> int) = of_nat n ==> P; !! n. z = - (of_nat (Suc n)) ==> P |] ==> P"
+ "[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P"
apply (cases "z < 0")
apply (blast dest!: negD)
apply (simp add: linorder_not_less del: of_nat_Suc)
@@ -562,12 +565,12 @@
done
theorem int_of_nat_induct [case_names nonneg neg, induct type: int]:
- "[|!! n. P (of_nat n \<Colon> int); !!n. P (- (of_nat (Suc n))) |] ==> P z"
+ "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z"
by (cases z) auto
text{*Contributed by Brian Huffman*}
theorem int_diff_cases:
- obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n"
+ obtains (diff) m n where "z = int m - int n"
apply (cases z rule: eq_Abs_Integ)
apply (rule_tac m=x and n=y in diff)
apply (simp add: int_def minus add diff_minus)
@@ -944,11 +947,11 @@
assumes number_of_eq: "number_of k = of_int k"
class number_semiring = number + comm_semiring_1 +
- assumes number_of_int: "number_of (of_nat n) = of_nat n"
+ assumes number_of_int: "number_of (int n) = of_nat n"
instance number_ring \<subseteq> number_semiring
proof
- fix n show "number_of (of_nat n) = (of_nat n :: 'a)"
+ fix n show "number_of (int n) = (of_nat n :: 'a)"
unfolding number_of_eq by (rule of_int_of_nat_eq)
qed
@@ -1124,7 +1127,7 @@
show ?thesis
proof
assume eq: "1 + z + z = 0"
- have "(0::int) < 1 + (of_nat n + of_nat n)"
+ have "(0::int) < 1 + (int n + int n)"
by (simp add: le_imp_0_less add_increasing)
also have "... = - (1 + z + z)"
by (simp add: neg add_assoc [symmetric])
@@ -1644,7 +1647,7 @@
lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
lemma split_nat [arith_split]:
- "P(nat(i::int)) = ((\<forall>n. i = of_nat n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
+ "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
(is "?P = (?L & ?R)")
proof (cases "i < 0")
case True thus ?thesis by auto
@@ -1737,11 +1740,6 @@
by (rule wf_subset [OF wf_measure])
qed
-abbreviation
- int :: "nat \<Rightarrow> int"
-where
- "int \<equiv> of_nat"
-
(* `set:int': dummy construction *)
theorem int_ge_induct [case_names base step, induct set: int]:
fixes i :: int
--- a/src/HOL/NSA/NSComplex.thy Mon Sep 05 19:18:38 2011 +0200
+++ b/src/HOL/NSA/NSComplex.thy Tue Sep 06 07:23:45 2011 +0200
@@ -613,7 +613,7 @@
by (simp add: NSDeMoivre_ext)
lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)"
-by transfer (rule expi_add)
+by transfer (rule exp_add)
subsection{*@{term hcomplex_of_complex}: the Injection from
--- a/src/HOL/Nominal/Nominal.thy Mon Sep 05 19:18:38 2011 +0200
+++ b/src/HOL/Nominal/Nominal.thy Tue Sep 06 07:23:45 2011 +0200
@@ -51,16 +51,16 @@
begin
definition
- perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) = (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
+ "perm_fun pi f = (\<lambda>x. pi \<bullet> f (rev pi \<bullet> x))"
definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
- perm_bool_def: "perm_bool pi b = b"
+ "perm_bool pi b = b"
primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit" where
"perm_unit pi () = ()"
primrec perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" where
- "perm_prod pi (x,y) = (pi\<bullet>x,pi\<bullet>y)"
+ "perm_prod pi (x, y) = (pi\<bullet>x, pi\<bullet>y)"
primrec perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" where
nil_eqvt: "perm_list pi [] = []"
@@ -71,13 +71,13 @@
| none_eqvt: "perm_option pi None = None"
definition perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char" where
- perm_char_def: "perm_char pi c = c"
+ "perm_char pi c = c"
definition perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat" where
- perm_nat_def: "perm_nat pi i = i"
+ "perm_nat pi i = i"
definition perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int" where
- perm_int_def: "perm_int pi i = i"
+ "perm_int pi i = i"
primrec perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" where
nsome_eqvt: "perm_noption pi (nSome x) = nSome (pi\<bullet>x)"
@@ -962,7 +962,7 @@
fixes pi::"'y prm"
and x ::"'x set"
assumes dj: "disjoint TYPE('x) TYPE('y)"
- shows "(pi\<bullet>x)=x"
+ shows "pi\<bullet>x=x"
using dj by (simp_all add: perm_fun_def disjoint_def perm_bool)
lemma dj_perm_perm_forget:
@@ -1028,7 +1028,7 @@
qed
lemma pt_unit_inst:
- shows "pt TYPE(unit) TYPE('x)"
+ shows "pt TYPE(unit) TYPE('x)"
by (simp add: pt_def)
lemma pt_prod_inst:
--- a/src/HOL/RComplete.thy Mon Sep 05 19:18:38 2011 +0200
+++ b/src/HOL/RComplete.thy Tue Sep 06 07:23:45 2011 +0200
@@ -475,12 +475,12 @@
unfolding natceiling_def real_of_nat_def
by (simp add: nat_le_iff ceiling_le_iff)
-lemma natceiling_le_eq: "0 <= x ==> (natceiling x <= a) = (x <= real a)"
- unfolding natceiling_def real_of_nat_def (* FIXME: unused assumption *)
+lemma natceiling_le_eq: "(natceiling x <= a) = (x <= real a)"
+ unfolding natceiling_def real_of_nat_def
by (simp add: nat_le_iff ceiling_le_iff)
lemma natceiling_le_eq_number_of [simp]:
- "~ neg((number_of n)::int) ==> 0 <= x ==>
+ "~ neg((number_of n)::int) ==>
(natceiling x <= number_of n) = (x <= number_of n)"
by (simp add: natceiling_le_eq)
--- a/src/HOL/SEQ.thy Mon Sep 05 19:18:38 2011 +0200
+++ b/src/HOL/SEQ.thy Tue Sep 06 07:23:45 2011 +0200
@@ -380,22 +380,6 @@
shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
unfolding Bseq_conv_Bfun by (rule Bfun_inverse)
-lemma LIMSEQ_add_const: (* FIXME: delete *)
- fixes a :: "'a::real_normed_vector"
- shows "f ----> a ==> (%n.(f n + b)) ----> a + b"
-by (intro tendsto_intros)
-
-(* FIXME: delete *)
-lemma LIMSEQ_add_minus:
- fixes a b :: "'a::real_normed_vector"
- shows "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
-by (intro tendsto_intros)
-
-lemma LIMSEQ_diff_const: (* FIXME: delete *)
- fixes a b :: "'a::real_normed_vector"
- shows "f ----> a ==> (%n.(f n - b)) ----> a - b"
-by (intro tendsto_intros)
-
lemma LIMSEQ_diff_approach_zero:
fixes L :: "'a::real_normed_vector"
shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
@@ -438,7 +422,8 @@
lemma LIMSEQ_inverse_real_of_nat_add_minus:
"(%n. r + -inverse(real(Suc n))) ----> r"
- using LIMSEQ_add_minus [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto
+ using tendsto_add [OF tendsto_const
+ tendsto_minus [OF LIMSEQ_inverse_real_of_nat]] by auto
lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
"(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
@@ -673,7 +658,6 @@
"!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
-
text{* Use completeness of reals (supremum property)
to show that any bounded sequence has a least upper bound*}
@@ -684,15 +668,8 @@
subsubsection{*A Bounded and Monotonic Sequence Converges*}
-lemma lemma_converg1:
- "!!(X::nat=>real). [| \<forall>m. \<forall> n \<ge> m. X m \<le> X n;
- isLub (UNIV::real set) {x. \<exists>n. X n = x} (X ma)
- |] ==> \<forall>n \<ge> ma. X n = X ma"
-apply safe
-apply (drule_tac y = "X n" in isLubD2)
-apply (blast dest: order_antisym)+
-done
-
+(* TODO: delete *)
+(* FIXME: one use in NSA/HSEQ.thy *)
lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
unfolding tendsto_def eventually_sequentially
apply (rule_tac x = "X m" in exI, safe)
@@ -700,50 +677,45 @@
apply (drule spec, erule impE, auto)
done
-lemma lemma_converg2:
- "!!(X::nat=>real).
- [| \<forall>m. X m ~= U; isLub UNIV {x. \<exists>n. X n = x} U |] ==> \<forall>m. X m < U"
-apply safe
-apply (drule_tac y = "X m" in isLubD2)
-apply (auto dest!: order_le_imp_less_or_eq)
-done
-
-lemma lemma_converg3: "!!(X ::nat=>real). \<forall>m. X m \<le> U ==> isUb UNIV {x. \<exists>n. X n = x} U"
-by (rule setleI [THEN isUbI], auto)
+text {* A monotone sequence converges to its least upper bound. *}
-text{* FIXME: @{term "U - T < U"} is redundant *}
-lemma lemma_converg4: "!!(X::nat=> real).
- [| \<forall>m. X m ~= U;
- isLub UNIV {x. \<exists>n. X n = x} U;
- 0 < T;
- U + - T < U
- |] ==> \<exists>m. U + -T < X m & X m < U"
-apply (drule lemma_converg2, assumption)
-apply (rule ccontr, simp)
-apply (simp add: linorder_not_less)
-apply (drule lemma_converg3)
-apply (drule isLub_le_isUb, assumption)
-apply (auto dest: order_less_le_trans)
-done
+lemma isLub_mono_imp_LIMSEQ:
+ fixes X :: "nat \<Rightarrow> real"
+ assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
+ assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
+ shows "X ----> u"
+proof (rule LIMSEQ_I)
+ have 1: "\<forall>n. X n \<le> u"
+ using isLubD2 [OF u] by auto
+ have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y"
+ using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def)
+ hence 2: "\<forall>y<u. \<exists>n. y < X n"
+ by (metis not_le)
+ fix r :: real assume "0 < r"
+ hence "u - r < u" by simp
+ hence "\<exists>m. u - r < X m" using 2 by simp
+ then obtain m where "u - r < X m" ..
+ with X have "\<forall>n\<ge>m. u - r < X n"
+ by (fast intro: less_le_trans)
+ hence "\<exists>m. \<forall>n\<ge>m. u - r < X n" ..
+ thus "\<exists>m. \<forall>n\<ge>m. norm (X n - u) < r"
+ using 1 by (simp add: diff_less_eq add_commute)
+qed
text{*A standard proof of the theorem for monotone increasing sequence*}
lemma Bseq_mono_convergent:
"[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent (X::nat=>real)"
-apply (simp add: convergent_def)
-apply (frule Bseq_isLub, safe)
-apply (case_tac "\<exists>m. X m = U", auto)
-apply (blast dest: lemma_converg1 Bmonoseq_LIMSEQ)
-(* second case *)
-apply (rule_tac x = U in exI)
-apply (subst LIMSEQ_iff, safe)
-apply (frule lemma_converg2, assumption)
-apply (drule lemma_converg4, auto)
-apply (rule_tac x = m in exI, safe)
-apply (subgoal_tac "X m \<le> X n")
- prefer 2 apply blast
-apply (drule_tac x=n and P="%m. X m < U" in spec, arith)
-done
+proof -
+ assume "Bseq X"
+ then obtain u where u: "isLub UNIV {x. \<exists>n. X n = x} u"
+ using Bseq_isLub by fast
+ assume "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
+ with u have "X ----> u"
+ by (rule isLub_mono_imp_LIMSEQ)
+ thus "convergent X"
+ by (rule convergentI)
+qed
lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X"
by (simp add: Bseq_def)
--- a/src/HOL/Series.thy Mon Sep 05 19:18:38 2011 +0200
+++ b/src/HOL/Series.thy Tue Sep 06 07:23:45 2011 +0200
@@ -122,7 +122,7 @@
shows "f sums s ==> (\<lambda>n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"
apply (unfold sums_def)
apply (simp add: sumr_offset)
- apply (rule LIMSEQ_diff_const)
+ apply (rule tendsto_diff [OF _ tendsto_const])
apply (rule LIMSEQ_ignore_initial_segment)
apply assumption
done
@@ -166,7 +166,7 @@
proof -
from sumSuc[unfolded sums_def]
have "(\<lambda>i. \<Sum>n = Suc 0..<Suc i. f n) ----> l" unfolding setsum_reindex[OF inj_Suc] image_Suc_atLeastLessThan[symmetric] comp_def .
- from LIMSEQ_add_const[OF this, where b="f 0"]
+ from tendsto_add[OF this tendsto_const, where b="f 0"]
have "(\<lambda>i. \<Sum>n = 0..<Suc i. f n) ----> l + f 0" unfolding add_commute setsum_head_upt_Suc[OF zero_less_Suc] .
thus ?thesis unfolding sums_def by (rule LIMSEQ_imp_Suc)
qed
@@ -625,7 +625,7 @@
apply (simp add:diff_Suc split:nat.splits)
apply (blast intro: norm_ratiotest_lemma)
apply (rule_tac x = "Suc N" in exI, clarify)
-apply(simp cong:setsum_ivl_cong)
+apply(simp cong del: setsum_cong cong: setsum_ivl_cong)
done
lemma ratio_test:
--- a/src/HOL/Tools/SMT/smt_normalize.ML Mon Sep 05 19:18:38 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Tue Sep 06 07:23:45 2011 +0200
@@ -475,8 +475,7 @@
"op * = (%a b. nat (int a * int b))"
"op div = (%a b. nat (int a div int b))"
"op mod = (%a b. nat (int a mod int b))"
- by (auto intro!: ext simp add: nat_mult_distrib nat_div_distrib
- nat_mod_distrib)}
+ by (fastsimp simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+}
val ints = map mk_meta_eq @{lemma
"int 0 = 0"
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Mon Sep 05 19:18:38 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Tue Sep 06 07:23:45 2011 +0200
@@ -148,13 +148,11 @@
end
local
- fun equal_var cv (_, cu) = (cv aconvc cu)
-
fun prep (ct, vars) (maxidx, all_vars) =
let
val maxidx' = maxidx + maxidx_of ct + 1
- fun part (v as (i, cv)) =
+ fun part (i, cv) =
(case AList.lookup (op =) all_vars i of
SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu))
| NONE =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Sep 05 19:18:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Sep 06 07:23:45 2011 +0200
@@ -124,18 +124,6 @@
ss as _ :: _ => forall (is_prover_supported ctxt) ss
| _ => false
-(* "provers =" and "type_enc =" can be left out. The latter is a secret
- feature. *)
-fun check_and_repair_raw_param ctxt (name, value) =
- if is_known_raw_param name then
- (name, value)
- else if is_prover_list ctxt name andalso null value then
- ("provers", [name])
- else if can (type_enc_from_string Sound) name andalso null value then
- ("type_enc", [name])
- else
- error ("Unknown parameter: " ^ quote name ^ ".")
-
fun unalias_raw_param (name, value) =
case AList.lookup (op =) alias_params name of
SOME name' => (name', value)
@@ -148,6 +136,21 @@
| _ => value)
| NONE => (name, value)
+(* "provers =" and "type_enc =" can be left out. The latter is a secret
+ feature. *)
+fun normalize_raw_param ctxt =
+ unalias_raw_param
+ #> (fn (name, value) =>
+ if is_known_raw_param name then
+ (name, value)
+ else if is_prover_list ctxt name andalso null value then
+ ("provers", [name])
+ else if can (type_enc_from_string Sound) name andalso null value then
+ ("type_enc", [name])
+ else
+ error ("Unknown parameter: " ^ quote name ^ "."))
+
+
(* Ensure that type systems such as "mono_simple!" and "mono_guards?" are
handled correctly. *)
fun implode_param [s, "?"] = s ^ "?"
@@ -205,7 +208,10 @@
max_default_remote_threads)
|> implode_param
-val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
+fun set_default_raw_param param thy =
+ let val ctxt = Proof_Context.init_global thy in
+ thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param))
+ end
fun default_raw_params ctxt =
let val thy = Proof_Context.theory_of ctxt in
Data.get thy
@@ -224,7 +230,6 @@
fun extract_params mode default_params override_params =
let
- val override_params = map unalias_raw_param override_params
val raw_params = rev override_params @ rev default_params
val lookup = Option.map implode_param o AList.lookup (op =) raw_params
val lookup_string = the_default "" o lookup
@@ -294,15 +299,15 @@
timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
-fun get_params mode ctxt = extract_params mode (default_raw_params ctxt)
+fun get_params mode = extract_params mode o default_raw_params
fun default_params thy = get_params Normal thy o map (apsnd single)
(* Sledgehammer the given subgoal *)
val default_minimize_prover = Metis_Tactic.metisN
-val is_raw_param_relevant_for_minimize =
- member (op =) params_for_minimize o fst o unalias_raw_param
+fun is_raw_param_relevant_for_minimize (name, _) =
+ member (op =) params_for_minimize name
fun string_for_raw_param (key, values) =
key ^ (case implode_param values of "" => "" | value => " = " ^ value)
@@ -324,8 +329,7 @@
fun hammer_away override_params subcommand opt_i relevance_override state =
let
val ctxt = Proof.context_of state
- val override_params =
- override_params |> map (check_and_repair_raw_param ctxt)
+ val override_params = override_params |> map (normalize_raw_param ctxt)
in
if subcommand = runN then
let val i = the_default 1 opt_i in
@@ -368,8 +372,7 @@
(case default_raw_params ctxt |> rev of
[] => "none"
| params =>
- params |> map (check_and_repair_raw_param ctxt)
- |> map string_for_raw_param
+ params |> map string_for_raw_param
|> sort_strings |> cat_lines))
end))
--- a/src/HOL/Tools/monomorph.ML Mon Sep 05 19:18:38 2011 +0200
+++ b/src/HOL/Tools/monomorph.ML Tue Sep 06 07:23:45 2011 +0200
@@ -319,7 +319,7 @@
val (thm_infos, (known_grounds, subs)) = prepare schematic_consts_of rthms
in
if Symtab.is_empty known_grounds then
- (map (single o pair 0 o snd) rthms, ctxt)
+ (map (fn Ground thm => [(0, thm)] | _ => []) thm_infos, ctxt)
else
make_subst_ctxt ctxt thm_infos known_grounds subs
|> limit_rounds ctxt (collect_substitutions thm_infos)
--- a/src/HOL/Transcendental.thy Mon Sep 05 19:18:38 2011 +0200
+++ b/src/HOL/Transcendental.thy Tue Sep 06 07:23:45 2011 +0200
@@ -1999,7 +1999,7 @@
apply (drule tan_total_pos)
apply (cut_tac [2] y="-y" in tan_total_pos, safe)
apply (rule_tac [3] x = "-x" in exI)
-apply (auto intro!: exI)
+apply (auto del: exI intro!: exI)
done
lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
@@ -2009,7 +2009,7 @@
apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
apply (rule_tac [4] Rolle)
apply (rule_tac [2] Rolle)
-apply (auto intro!: DERIV_tan DERIV_isCont exI
+apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI
simp add: differentiable_def)
txt{*Now, simulate TRYALL*}
apply (rule_tac [!] DERIV_tan asm_rl)
@@ -2785,7 +2785,7 @@
have "norm (?diff 1 n - 0) < r" by auto }
thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
qed
- from this[unfolded tendsto_rabs_zero_iff diff_minus add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN tendsto_minus]
+ from this [unfolded tendsto_rabs_zero_iff, THEN tendsto_add [OF _ tendsto_const], of "- arctan 1", THEN tendsto_minus]
have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
--- a/src/HOL/Unix/Nested_Environment.thy Mon Sep 05 19:18:38 2011 +0200
+++ b/src/HOL/Unix/Nested_Environment.thy Tue Sep 06 07:23:45 2011 +0200
@@ -9,7 +9,7 @@
begin
text {*
- Consider a partial function @{term [source] "e :: 'a => 'b option"};
+ Consider a partial function @{term [source] "e :: 'a \<Rightarrow> 'b option"};
this may be understood as an \emph{environment} mapping indexes
@{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory
@{text Map} of Isabelle/HOL). This basic idea is easily generalized
@@ -21,7 +21,7 @@
datatype ('a, 'b, 'c) env =
Val 'a
- | Env 'b "'c => ('a, 'b, 'c) env option"
+ | Env 'b "'c \<Rightarrow> ('a, 'b, 'c) env option"
text {*
\medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ
@@ -43,14 +43,14 @@
@{term None}.
*}
-primrec lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
- and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option"
+primrec lookup :: "('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"
+ and lookup_option :: "('a, 'b, 'c) env option \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"
where
"lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
| "lookup (Env b es) xs =
(case xs of
- [] => Some (Env b es)
- | y # ys => lookup_option (es y) ys)"
+ [] \<Rightarrow> Some (Env b es)
+ | y # ys \<Rightarrow> lookup_option (es y) ys)"
| "lookup_option None xs = None"
| "lookup_option (Some e) xs = lookup e xs"
@@ -70,8 +70,8 @@
theorem lookup_env_cons:
"lookup (Env b es) (x # xs) =
(case es x of
- None => None
- | Some e => lookup e xs)"
+ None \<Rightarrow> None
+ | Some e \<Rightarrow> lookup e xs)"
by (cases "es x") simp_all
lemmas lookup_lookup_option.simps [simp del]
@@ -80,14 +80,14 @@
theorem lookup_eq:
"lookup env xs =
(case xs of
- [] => Some env
- | x # xs =>
+ [] \<Rightarrow> Some env
+ | x # xs \<Rightarrow>
(case env of
- Val a => None
- | Env b es =>
+ Val a \<Rightarrow> None
+ | Env b es \<Rightarrow>
(case es x of
- None => None
- | Some e => lookup e xs)))"
+ None \<Rightarrow> None
+ | Some e \<Rightarrow> lookup e xs)))"
by (simp split: list.split env.split)
text {*
@@ -245,18 +245,18 @@
environment is left unchanged.
*}
-primrec update :: "'c list => ('a, 'b, 'c) env option =>
- ('a, 'b, 'c) env => ('a, 'b, 'c) env"
- and update_option :: "'c list => ('a, 'b, 'c) env option =>
- ('a, 'b, 'c) env option => ('a, 'b, 'c) env option"
+primrec update :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>
+ ('a, 'b, 'c) env \<Rightarrow> ('a, 'b, 'c) env"
+ and update_option :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>
+ ('a, 'b, 'c) env option \<Rightarrow> ('a, 'b, 'c) env option"
where
"update xs opt (Val a) =
- (if xs = [] then (case opt of None => Val a | Some e => e)
+ (if xs = [] then (case opt of None \<Rightarrow> Val a | Some e \<Rightarrow> e)
else Val a)"
| "update xs opt (Env b es) =
(case xs of
- [] => (case opt of None => Env b es | Some e => e)
- | y # ys => Env b (es (y := update_option ys opt (es y))))"
+ [] \<Rightarrow> (case opt of None \<Rightarrow> Env b es | Some e \<Rightarrow> e)
+ | y # ys \<Rightarrow> Env b (es (y := update_option ys opt (es y))))"
| "update_option xs opt None =
(if xs = [] then opt else None)"
| "update_option xs opt (Some e) =
@@ -286,8 +286,8 @@
"update (x # y # ys) opt (Env b es) =
Env b (es (x :=
(case es x of
- None => None
- | Some e => Some (update (y # ys) opt e))))"
+ None \<Rightarrow> None
+ | Some e \<Rightarrow> Some (update (y # ys) opt e))))"
by (cases "es x") simp_all
lemmas update_update_option.simps [simp del]
@@ -297,21 +297,21 @@
lemma update_eq:
"update xs opt env =
(case xs of
- [] =>
+ [] \<Rightarrow>
(case opt of
- None => env
- | Some e => e)
- | x # xs =>
+ None \<Rightarrow> env
+ | Some e \<Rightarrow> e)
+ | x # xs \<Rightarrow>
(case env of
- Val a => Val a
- | Env b es =>
+ Val a \<Rightarrow> Val a
+ | Env b es \<Rightarrow>
(case xs of
- [] => Env b (es (x := opt))
- | y # ys =>
+ [] \<Rightarrow> Env b (es (x := opt))
+ | y # ys \<Rightarrow>
Env b (es (x :=
(case es x of
- None => None
- | Some e => Some (update (y # ys) opt e)))))))"
+ None \<Rightarrow> None
+ | Some e \<Rightarrow> Some (update (y # ys) opt e)))))))"
by (simp split: list.split env.split option.split)
text {*
--- a/src/Pure/General/markup.ML Mon Sep 05 19:18:38 2011 +0200
+++ b/src/Pure/General/markup.ML Tue Sep 06 07:23:45 2011 +0200
@@ -58,7 +58,6 @@
val propN: string val prop: T
val ML_keywordN: string val ML_keyword: T
val ML_delimiterN: string val ML_delimiter: T
- val ML_identN: string val ML_ident: T
val ML_tvarN: string val ML_tvar: T
val ML_numeralN: string val ML_numeral: T
val ML_charN: string val ML_char: T
@@ -80,7 +79,6 @@
val keywordN: string val keyword: T
val operatorN: string val operator: T
val commandN: string val command: T
- val identN: string val ident: T
val stringN: string val string: T
val altstringN: string val altstring: T
val verbatimN: string val verbatim: T
@@ -257,7 +255,6 @@
val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
-val (ML_identN, ML_ident) = markup_elem "ML_ident";
val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
val (ML_charN, ML_char) = markup_elem "ML_char";
@@ -292,7 +289,6 @@
val (keywordN, keyword) = markup_elem "keyword";
val (operatorN, operator) = markup_elem "operator";
val (commandN, command) = markup_elem "command";
-val (identN, ident) = markup_elem "ident";
val (stringN, string) = markup_elem "string";
val (altstringN, altstring) = markup_elem "altstring";
val (verbatimN, verbatim) = markup_elem "verbatim";
--- a/src/Pure/General/markup.scala Mon Sep 05 19:18:38 2011 +0200
+++ b/src/Pure/General/markup.scala Tue Sep 06 07:23:45 2011 +0200
@@ -142,7 +142,6 @@
val ML_KEYWORD = "ML_keyword"
val ML_DELIMITER = "ML_delimiter"
- val ML_IDENT = "ML_ident"
val ML_TVAR = "ML_tvar"
val ML_NUMERAL = "ML_numeral"
val ML_CHAR = "ML_char"
@@ -164,7 +163,6 @@
val KEYWORD = "keyword"
val OPERATOR = "operator"
val COMMAND = "command"
- val IDENT = "ident"
val STRING = "string"
val ALTSTRING = "altstring"
val VERBATIM = "verbatim"
--- a/src/Pure/General/timing.scala Mon Sep 05 19:18:38 2011 +0200
+++ b/src/Pure/General/timing.scala Tue Sep 06 07:23:45 2011 +0200
@@ -9,6 +9,7 @@
object Time
{
def seconds(s: Double): Time = new Time((s * 1000.0) round)
+ def ms(m: Long): Time = new Time(m)
}
class Time(val ms: Long)
--- a/src/Pure/General/xml.ML Mon Sep 05 19:18:38 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,361 +0,0 @@
-(* Title: Pure/General/xml.ML
- Author: David Aspinall, Stefan Berghofer and Markus Wenzel
-
-Untyped XML trees.
-*)
-
-signature XML_DATA_OPS =
-sig
- type 'a A
- type 'a T
- type 'a V
- val int_atom: int A
- val bool_atom: bool A
- val unit_atom: unit A
- val properties: Properties.T T
- val string: string T
- val int: int T
- val bool: bool T
- val unit: unit T
- val pair: 'a T -> 'b T -> ('a * 'b) T
- val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
- val list: 'a T -> 'a list T
- val option: 'a T -> 'a option T
- val variant: 'a V list -> 'a T
-end;
-
-signature XML =
-sig
- type attributes = Properties.T
- datatype tree =
- Elem of Markup.T * tree list
- | Text of string
- type body = tree list
- val add_content: tree -> Buffer.T -> Buffer.T
- val content_of: body -> string
- val header: string
- val text: string -> string
- val element: string -> attributes -> string list -> string
- val output_markup: Markup.T -> Output.output * Output.output
- val string_of: tree -> string
- val pretty: int -> tree -> Pretty.T
- val output: tree -> TextIO.outstream -> unit
- val parse_comments: string list -> unit * string list
- val parse_string : string -> string option
- val parse_element: string list -> tree * string list
- val parse_document: string list -> tree * string list
- val parse: string -> tree
- exception XML_ATOM of string
- exception XML_BODY of body
- structure Encode: XML_DATA_OPS
- structure Decode: XML_DATA_OPS
-end;
-
-structure XML: XML =
-struct
-
-(** XML trees **)
-
-type attributes = Properties.T;
-
-datatype tree =
- Elem of Markup.T * tree list
- | Text of string;
-
-type body = tree list;
-
-fun add_content (Elem (_, ts)) = fold add_content ts
- | add_content (Text s) = Buffer.add s;
-
-fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
-
-
-
-(** string representation **)
-
-val header = "<?xml version=\"1.0\"?>\n";
-
-
-(* escaped text *)
-
-fun decode "<" = "<"
- | decode ">" = ">"
- | decode "&" = "&"
- | decode "'" = "'"
- | decode """ = "\""
- | decode c = c;
-
-fun encode "<" = "<"
- | encode ">" = ">"
- | encode "&" = "&"
- | encode "'" = "'"
- | encode "\"" = """
- | encode c = c;
-
-val text = translate_string encode;
-
-
-(* elements *)
-
-fun elem name atts =
- space_implode " " (name :: map (fn (a, x) => a ^ "=\"" ^ text x ^ "\"") atts);
-
-fun element name atts body =
- let val b = implode body in
- if b = "" then enclose "<" "/>" (elem name atts)
- else enclose "<" ">" (elem name atts) ^ b ^ enclose "</" ">" name
- end;
-
-fun output_markup (markup as (name, atts)) =
- if Markup.is_empty markup then Markup.no_output
- else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
-
-
-(* output *)
-
-fun buffer_of depth tree =
- let
- fun traverse _ (Elem ((name, atts), [])) =
- Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
- | traverse d (Elem ((name, atts), ts)) =
- Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
- traverse_body d ts #>
- Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
- | traverse _ (Text s) = Buffer.add (text s)
- and traverse_body 0 _ = Buffer.add "..."
- | traverse_body d ts = fold (traverse (d - 1)) ts;
- in Buffer.empty |> traverse depth tree end;
-
-val string_of = Buffer.content o buffer_of ~1;
-val output = Buffer.output o buffer_of ~1;
-
-fun pretty depth tree =
- Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
-
-
-
-(** XML parsing (slow) **)
-
-local
-
-fun err msg (xs, _) =
- fn () => "XML parsing error: " ^ msg () ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
-
-fun ignored _ = [];
-
-val blanks = Scan.many Symbol.is_blank;
-val special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
-val regular = Scan.one Symbol.is_regular;
-fun regular_except x = Scan.one (fn c => Symbol.is_regular c andalso c <> x);
-
-val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode;
-
-val parse_cdata =
- Scan.this_string "<![CDATA[" |--
- (Scan.repeat (Scan.unless (Scan.this_string "]]>") regular) >> implode) --|
- Scan.this_string "]]>";
-
-val parse_att =
- (Symbol.scan_id --| (blanks -- $$ "=" -- blanks)) --
- (($$ "\"" || $$ "'") :|-- (fn s =>
- (Scan.repeat (special || regular_except s) >> implode) --| $$ s));
-
-val parse_comment =
- Scan.this_string "<!--" --
- Scan.repeat (Scan.unless (Scan.this_string "-->") regular) --
- Scan.this_string "-->" >> ignored;
-
-val parse_processing_instruction =
- Scan.this_string "<?" --
- Scan.repeat (Scan.unless (Scan.this_string "?>") regular) --
- Scan.this_string "?>" >> ignored;
-
-val parse_doctype =
- Scan.this_string "<!DOCTYPE" --
- Scan.repeat (Scan.unless ($$ ">") regular) --
- $$ ">" >> ignored;
-
-val parse_misc =
- Scan.one Symbol.is_blank >> ignored ||
- parse_processing_instruction ||
- parse_comment;
-
-val parse_optional_text =
- Scan.optional (parse_chars >> (single o Text)) [];
-
-fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_";
-fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = ".";
-val parse_name = Scan.one name_start_char ::: Scan.many name_char;
-
-in
-
-val parse_comments =
- blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K ();
-
-val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode;
-
-fun parse_content xs =
- (parse_optional_text @@@
- (Scan.repeat
- ((parse_element >> single ||
- parse_cdata >> (single o Text) ||
- parse_processing_instruction ||
- parse_comment)
- @@@ parse_optional_text) >> flat)) xs
-
-and parse_element xs =
- ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--
- (fn (name, _) =>
- !! (err (fn () => "Expected > or />"))
- ($$ "/" -- $$ ">" >> ignored ||
- $$ ">" |-- parse_content --|
- !! (err (fn () => "Expected </" ^ implode name ^ ">"))
- ($$ "<" -- $$ "/" -- Scan.this name -- blanks -- $$ ">")))
- >> (fn ((name, atts), body) => Elem ((implode name, atts), body))) xs;
-
-val parse_document =
- (Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc)
- |-- parse_element;
-
-fun parse s =
- (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element"))
- (blanks |-- parse_document --| blanks))) (raw_explode s) of
- (x, []) => x
- | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));
-
-end;
-
-
-
-(** XML as data representation language **)
-
-exception XML_ATOM of string;
-exception XML_BODY of tree list;
-
-
-structure Encode =
-struct
-
-type 'a A = 'a -> string;
-type 'a T = 'a -> body;
-type 'a V = 'a -> string list * body;
-
-
-(* atomic values *)
-
-fun int_atom i = signed_string_of_int i;
-
-fun bool_atom false = "0"
- | bool_atom true = "1";
-
-fun unit_atom () = "";
-
-
-(* structural nodes *)
-
-fun node ts = Elem ((":", []), ts);
-
-fun vector xs = map_index (fn (i, x) => (int_atom i, x)) xs;
-
-fun tagged (tag, (xs, ts)) = Elem ((int_atom tag, vector xs), ts);
-
-
-(* representation of standard types *)
-
-fun properties props = [Elem ((":", props), [])];
-
-fun string "" = []
- | string s = [Text s];
-
-val int = string o int_atom;
-
-val bool = string o bool_atom;
-
-val unit = string o unit_atom;
-
-fun pair f g (x, y) = [node (f x), node (g y)];
-
-fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
-
-fun list f xs = map (node o f) xs;
-
-fun option _ NONE = []
- | option f (SOME x) = [node (f x)];
-
-fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
-
-end;
-
-
-structure Decode =
-struct
-
-type 'a A = string -> 'a;
-type 'a T = body -> 'a;
-type 'a V = string list * body -> 'a;
-
-
-(* atomic values *)
-
-fun int_atom s =
- Markup.parse_int s
- handle Fail _ => raise XML_ATOM s;
-
-fun bool_atom "0" = false
- | bool_atom "1" = true
- | bool_atom s = raise XML_ATOM s;
-
-fun unit_atom "" = ()
- | unit_atom s = raise XML_ATOM s;
-
-
-(* structural nodes *)
-
-fun node (Elem ((":", []), ts)) = ts
- | node t = raise XML_BODY [t];
-
-fun vector atts =
- #1 (fold_map (fn (a, x) =>
- fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts 0);
-
-fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
- | tagged t = raise XML_BODY [t];
-
-
-(* representation of standard types *)
-
-fun properties [Elem ((":", props), [])] = props
- | properties ts = raise XML_BODY ts;
-
-fun string [] = ""
- | string [Text s] = s
- | string ts = raise XML_BODY ts;
-
-val int = int_atom o string;
-
-val bool = bool_atom o string;
-
-val unit = unit_atom o string;
-
-fun pair f g [t1, t2] = (f (node t1), g (node t2))
- | pair _ _ ts = raise XML_BODY ts;
-
-fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
- | triple _ _ _ ts = raise XML_BODY ts;
-
-fun list f ts = map (f o node) ts;
-
-fun option _ [] = NONE
- | option f [t] = SOME (f (node t))
- | option _ ts = raise XML_BODY ts;
-
-fun variant fs [t] =
- let
- val (tag, (xs, ts)) = tagged t;
- val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
- in f (xs, ts) end
- | variant _ ts = raise XML_BODY ts;
-
-end;
-
-end;
--- a/src/Pure/General/xml.scala Mon Sep 05 19:18:38 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,390 +0,0 @@
-/* Title: Pure/General/xml.scala
- Author: Makarius
-
-Untyped XML trees.
-*/
-
-package isabelle
-
-import java.lang.System
-import java.util.WeakHashMap
-import java.lang.ref.WeakReference
-import javax.xml.parsers.DocumentBuilderFactory
-
-import scala.actors.Actor._
-import scala.collection.mutable
-
-
-object XML
-{
- /** XML trees **/
-
- /* datatype representation */
-
- type Attributes = Properties.T
-
- sealed abstract class Tree { override def toString = string_of_tree(this) }
- case class Elem(markup: Markup, body: List[Tree]) extends Tree
- case class Text(content: String) extends Tree
-
- def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
- def elem(name: String) = Elem(Markup(name, Nil), Nil)
-
- type Body = List[Tree]
-
-
- /* string representation */
-
- def string_of_body(body: Body): String =
- {
- val s = new StringBuilder
-
- def text(txt: String) {
- if (txt == null) s ++= txt
- else {
- for (c <- txt.iterator) c match {
- case '<' => s ++= "<"
- case '>' => s ++= ">"
- case '&' => s ++= "&"
- case '"' => s ++= """
- case '\'' => s ++= "'"
- case _ => s += c
- }
- }
- }
- def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
- def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
- def tree(t: Tree): Unit =
- t match {
- case Elem(markup, Nil) =>
- s ++= "<"; elem(markup); s ++= "/>"
- case Elem(markup, ts) =>
- s ++= "<"; elem(markup); s ++= ">"
- ts.foreach(tree)
- s ++= "</"; s ++= markup.name; s ++= ">"
- case Text(txt) => text(txt)
- }
- body.foreach(tree)
- s.toString
- }
-
- def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
-
-
- /* text content */
-
- def content_stream(tree: Tree): Stream[String] =
- tree match {
- case Elem(_, body) => content_stream(body)
- case Text(content) => Stream(content)
- }
- def content_stream(body: Body): Stream[String] =
- body.toStream.flatten(content_stream(_))
-
- def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
- def content(body: Body): Iterator[String] = content_stream(body).iterator
-
-
- /* pipe-lined cache for partial sharing */
-
- class Cache(initial_size: Int = 131071, max_string: Int = 100)
- {
- private val cache_actor = actor
- {
- val table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
-
- def lookup[A](x: A): Option[A] =
- {
- val ref = table.get(x)
- if (ref == null) None
- else {
- val y = ref.asInstanceOf[WeakReference[A]].get
- if (y == null) None
- else Some(y)
- }
- }
- def store[A](x: A): A =
- {
- table.put(x, new WeakReference[Any](x))
- x
- }
-
- def trim_bytes(s: String): String = new String(s.toCharArray)
-
- def cache_string(x: String): String =
- lookup(x) match {
- case Some(y) => y
- case None =>
- val z = trim_bytes(x)
- if (z.length > max_string) z else store(z)
- }
- def cache_props(x: Properties.T): Properties.T =
- if (x.isEmpty) x
- else
- lookup(x) match {
- case Some(y) => y
- case None => store(x.map(p => (trim_bytes(p._1).intern, cache_string(p._2))))
- }
- def cache_markup(x: Markup): Markup =
- lookup(x) match {
- case Some(y) => y
- case None =>
- x match {
- case Markup(name, props) =>
- store(Markup(cache_string(name), cache_props(props)))
- }
- }
- def cache_tree(x: XML.Tree): XML.Tree =
- lookup(x) match {
- case Some(y) => y
- case None =>
- x match {
- case XML.Elem(markup, body) =>
- store(XML.Elem(cache_markup(markup), cache_body(body)))
- case XML.Text(text) => store(XML.Text(cache_string(text)))
- }
- }
- def cache_body(x: XML.Body): XML.Body =
- if (x.isEmpty) x
- else
- lookup(x) match {
- case Some(y) => y
- case None => x.map(cache_tree(_))
- }
-
- // main loop
- loop {
- react {
- case Cache_String(x, f) => f(cache_string(x))
- case Cache_Markup(x, f) => f(cache_markup(x))
- case Cache_Tree(x, f) => f(cache_tree(x))
- case Cache_Body(x, f) => f(cache_body(x))
- case Cache_Ignore(x, f) => f(x)
- case bad => System.err.println("XML.cache_actor: ignoring bad input " + bad)
- }
- }
- }
-
- private case class Cache_String(x: String, f: String => Unit)
- private case class Cache_Markup(x: Markup, f: Markup => Unit)
- private case class Cache_Tree(x: XML.Tree, f: XML.Tree => Unit)
- private case class Cache_Body(x: XML.Body, f: XML.Body => Unit)
- private case class Cache_Ignore[A](x: A, f: A => Unit)
-
- // main methods
- def cache_string(x: String)(f: String => Unit) { cache_actor ! Cache_String(x, f) }
- def cache_markup(x: Markup)(f: Markup => Unit) { cache_actor ! Cache_Markup(x, f) }
- def cache_tree(x: XML.Tree)(f: XML.Tree => Unit) { cache_actor ! Cache_Tree(x, f) }
- def cache_body(x: XML.Body)(f: XML.Body => Unit) { cache_actor ! Cache_Body(x, f) }
- def cache_ignore[A](x: A)(f: A => Unit) { cache_actor ! Cache_Ignore(x, f) }
- }
-
-
-
- /** document object model (W3C DOM) **/
-
- def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
- node.getUserData(Markup.Data.name) match {
- case tree: XML.Tree => Some(tree)
- case _ => None
- }
-
- def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
- {
- def DOM(tr: Tree): org.w3c.dom.Node = tr match {
- case Elem(Markup.Data, List(data, t)) =>
- val node = DOM(t)
- node.setUserData(Markup.Data.name, data, null)
- node
- case Elem(Markup(name, atts), ts) =>
- if (name == Markup.Data.name)
- error("Malformed data element: " + tr.toString)
- val node = doc.createElement(name)
- for ((name, value) <- atts) node.setAttribute(name, value)
- for (t <- ts) node.appendChild(DOM(t))
- node
- case Text(txt) => doc.createTextNode(txt)
- }
- DOM(tree)
- }
-
-
-
- /** XML as data representation language **/
-
- class XML_Atom(s: String) extends Exception(s)
- class XML_Body(body: XML.Body) extends Exception
-
- object Encode
- {
- type T[A] = A => XML.Body
-
-
- /* atomic values */
-
- def long_atom(i: Long): String = i.toString
-
- def int_atom(i: Int): String = i.toString
-
- def bool_atom(b: Boolean): String = if (b) "1" else "0"
-
- def unit_atom(u: Unit) = ""
-
-
- /* structural nodes */
-
- private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
-
- private def vector(xs: List[String]): XML.Attributes =
- xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
-
- private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
- XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
-
-
- /* representation of standard types */
-
- val properties: T[Properties.T] =
- (props => List(XML.Elem(Markup(":", props), Nil)))
-
- val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
-
- val long: T[Long] = (x => string(long_atom(x)))
-
- val int: T[Int] = (x => string(int_atom(x)))
-
- val bool: T[Boolean] = (x => string(bool_atom(x)))
-
- val unit: T[Unit] = (x => string(unit_atom(x)))
-
- def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
- (x => List(node(f(x._1)), node(g(x._2))))
-
- def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
- (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
-
- def list[A](f: T[A]): T[List[A]] =
- (xs => xs.map((x: A) => node(f(x))))
-
- def option[A](f: T[A]): T[Option[A]] =
- {
- case None => Nil
- case Some(x) => List(node(f(x)))
- }
-
- def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
- {
- case x =>
- val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
- List(tagged(tag, f(x)))
- }
- }
-
- object Decode
- {
- type T[A] = XML.Body => A
- type V[A] = (List[String], XML.Body) => A
-
-
- /* atomic values */
-
- def long_atom(s: String): Long =
- try { java.lang.Long.parseLong(s) }
- catch { case e: NumberFormatException => throw new XML_Atom(s) }
-
- def int_atom(s: String): Int =
- try { Integer.parseInt(s) }
- catch { case e: NumberFormatException => throw new XML_Atom(s) }
-
- def bool_atom(s: String): Boolean =
- if (s == "1") true
- else if (s == "0") false
- else throw new XML_Atom(s)
-
- def unit_atom(s: String): Unit =
- if (s == "") () else throw new XML_Atom(s)
-
-
- /* structural nodes */
-
- private def node(t: XML.Tree): XML.Body =
- t match {
- case XML.Elem(Markup(":", Nil), ts) => ts
- case _ => throw new XML_Body(List(t))
- }
-
- private def vector(atts: XML.Attributes): List[String] =
- {
- val xs = new mutable.ListBuffer[String]
- var i = 0
- for ((a, x) <- atts) {
- if (int_atom(a) == i) { xs += x; i = i + 1 }
- else throw new XML_Atom(a)
- }
- xs.toList
- }
-
- private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
- t match {
- case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
- case _ => throw new XML_Body(List(t))
- }
-
-
- /* representation of standard types */
-
- val properties: T[Properties.T] =
- {
- case List(XML.Elem(Markup(":", props), Nil)) => props
- case ts => throw new XML_Body(ts)
- }
-
- val string: T[String] =
- {
- case Nil => ""
- case List(XML.Text(s)) => s
- case ts => throw new XML_Body(ts)
- }
-
- val long: T[Long] = (x => long_atom(string(x)))
-
- val int: T[Int] = (x => int_atom(string(x)))
-
- val bool: T[Boolean] = (x => bool_atom(string(x)))
-
- val unit: T[Unit] = (x => unit_atom(string(x)))
-
- def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
- {
- case List(t1, t2) => (f(node(t1)), g(node(t2)))
- case ts => throw new XML_Body(ts)
- }
-
- def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
- {
- case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
- case ts => throw new XML_Body(ts)
- }
-
- def list[A](f: T[A]): T[List[A]] =
- (ts => ts.map(t => f(node(t))))
-
- def option[A](f: T[A]): T[Option[A]] =
- {
- case Nil => None
- case List(t) => Some(f(node(t)))
- case ts => throw new XML_Body(ts)
- }
-
- def variant[A](fs: List[V[A]]): T[A] =
- {
- case List(t) =>
- val (tag, (xs, ts)) = tagged(t)
- val f =
- try { fs(tag) }
- catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
- f(xs, ts)
- case ts => throw new XML_Body(ts)
- }
- }
-}
--- a/src/Pure/General/yxml.ML Mon Sep 05 19:18:38 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,147 +0,0 @@
-(* Title: Pure/General/yxml.ML
- Author: Makarius
-
-Efficient text representation of XML trees using extra characters X
-and Y -- no escaping, may nest marked text verbatim.
-
-Markup <elem att="val" ...>...body...</elem> is encoded as:
-
- X Y name Y att=val ... X
- ...
- body
- ...
- X Y X
-*)
-
-signature YXML =
-sig
- val X: Symbol.symbol
- val Y: Symbol.symbol
- val embed_controls: string -> string
- val detect: string -> bool
- val output_markup: Markup.T -> string * string
- val element: string -> XML.attributes -> string list -> string
- val string_of_body: XML.body -> string
- val string_of: XML.tree -> string
- val parse_body: string -> XML.body
- val parse: string -> XML.tree
-end;
-
-structure YXML: YXML =
-struct
-
-(** string representation **)
-
-(* idempotent recoding of certain low ASCII control characters *)
-
-fun pseudo_utf8 c =
- if Symbol.is_ascii_control c
- then chr 192 ^ chr (128 + ord c)
- else c;
-
-fun embed_controls str =
- if exists_string Symbol.is_ascii_control str
- then translate_string pseudo_utf8 str
- else str;
-
-
-(* markers *)
-
-val X = chr 5;
-val Y = chr 6;
-val XY = X ^ Y;
-val XYX = XY ^ X;
-
-val detect = exists_string (fn s => s = X orelse s = Y);
-
-
-(* output *)
-
-fun output_markup (markup as (name, atts)) =
- if Markup.is_empty markup then Markup.no_output
- else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
-
-fun element name atts body =
- let val (pre, post) = output_markup (name, atts)
- in pre ^ implode body ^ post end;
-
-fun string_of_body body =
- let
- fun attrib (a, x) =
- Buffer.add Y #>
- Buffer.add a #> Buffer.add "=" #> Buffer.add x;
- fun tree (XML.Elem ((name, atts), ts)) =
- Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
- trees ts #>
- Buffer.add XYX
- | tree (XML.Text s) = Buffer.add s
- and trees ts = fold tree ts;
- in Buffer.empty |> trees body |> Buffer.content end;
-
-val string_of = string_of_body o single;
-
-
-
-(** efficient YXML parsing **)
-
-local
-
-(* splitting *)
-
-fun is_char s c = ord s = Char.ord c;
-
-val split_string =
- Substring.full #>
- Substring.tokens (is_char X) #>
- map (Substring.fields (is_char Y) #> map Substring.string);
-
-
-(* structural errors *)
-
-fun err msg = raise Fail ("Malformed YXML encoding: " ^ msg);
-fun err_attribute () = err "bad attribute";
-fun err_element () = err "bad element";
-fun err_unbalanced "" = err "unbalanced element"
- | err_unbalanced name = err ("unbalanced element " ^ quote name);
-
-
-(* stack operations *)
-
-fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending;
-
-fun push "" _ _ = err_element ()
- | push name atts pending = ((name, atts), []) :: pending;
-
-fun pop ((("", _), _) :: _) = err_unbalanced ""
- | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
-
-
-(* parsing *)
-
-fun parse_attrib s =
- (case first_field "=" s of
- NONE => err_attribute ()
- | SOME ("", _) => err_attribute ()
- | SOME att => att);
-
-fun parse_chunk ["", ""] = pop
- | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
- | parse_chunk txts = fold (add o XML.Text) txts;
-
-in
-
-fun parse_body source =
- (case fold parse_chunk (split_string source) [(("", []), [])] of
- [(("", _), result)] => rev result
- | ((name, _), _) :: _ => err_unbalanced name);
-
-fun parse source =
- (case parse_body source of
- [result] => result
- | [] => XML.Text ""
- | _ => err "multiple results");
-
-end;
-
-end;
-
--- a/src/Pure/General/yxml.scala Mon Sep 05 19:18:38 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,134 +0,0 @@
-/* Title: Pure/General/yxml.scala
- Author: Makarius
-
-Efficient text representation of XML trees.
-*/
-
-package isabelle
-
-
-import scala.collection.mutable
-
-
-object YXML
-{
- /* chunk markers */
-
- val X = '\5'
- val Y = '\6'
- val X_string = X.toString
- val Y_string = Y.toString
-
- def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
-
-
- /* string representation */ // FIXME byte array version with pseudo-utf-8 (!?)
-
- def string_of_body(body: XML.Body): String =
- {
- val s = new StringBuilder
- def attrib(p: (String, String)) { s += Y; s ++= p._1; s += '='; s ++= p._2 }
- def tree(t: XML.Tree): Unit =
- t match {
- case XML.Elem(Markup(name, atts), ts) =>
- s += X; s += Y; s++= name; atts.foreach(attrib); s += X
- ts.foreach(tree)
- s += X; s += Y; s += X
- case XML.Text(text) => s ++= text
- }
- body.foreach(tree)
- s.toString
- }
-
- def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
-
-
- /* parsing */
-
- private def err(msg: String) = error("Malformed YXML: " + msg)
- private def err_attribute() = err("bad attribute")
- private def err_element() = err("bad element")
- private def err_unbalanced(name: String) =
- if (name == "") err("unbalanced element")
- else err("unbalanced element " + quote(name))
-
- private def parse_attrib(source: CharSequence) = {
- val s = source.toString
- val i = s.indexOf('=')
- if (i <= 0) err_attribute()
- (s.substring(0, i), s.substring(i + 1))
- }
-
-
- def parse_body(source: CharSequence): XML.Body =
- {
- /* stack operations */
-
- def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
- var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
-
- def add(x: XML.Tree)
- {
- (stack: @unchecked) match { case ((_, body) :: _) => body += x }
- }
-
- def push(name: String, atts: XML.Attributes)
- {
- if (name == "") err_element()
- else stack = (Markup(name, atts), buffer()) :: stack
- }
-
- def pop()
- {
- (stack: @unchecked) match {
- case ((Markup.Empty, _) :: _) => err_unbalanced("")
- case ((markup, body) :: pending) =>
- stack = pending
- add(XML.Elem(markup, body.toList))
- }
- }
-
-
- /* parse chunks */
-
- for (chunk <- Library.chunks(source, X) if chunk.length != 0) {
- if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
- else {
- Library.chunks(chunk, Y).toList match {
- case ch :: name :: atts if ch.length == 0 =>
- push(name.toString, atts.map(parse_attrib))
- case txts => for (txt <- txts) add(XML.Text(txt.toString))
- }
- }
- }
- (stack: @unchecked) match {
- case List((Markup.Empty, body)) => body.toList
- case (Markup(name, _), _) :: _ => err_unbalanced(name)
- }
- }
-
- def parse(source: CharSequence): XML.Tree =
- parse_body(source) match {
- case List(result) => result
- case Nil => XML.Text("")
- case _ => err("multiple results")
- }
-
-
- /* failsafe parsing */
-
- private def markup_malformed(source: CharSequence) =
- XML.elem(Markup.MALFORMED, List(XML.Text(source.toString)))
-
- def parse_body_failsafe(source: CharSequence): XML.Body =
- {
- try { parse_body(source) }
- catch { case ERROR(_) => List(markup_malformed(source)) }
- }
-
- def parse_failsafe(source: CharSequence): XML.Tree =
- {
- try { parse(source) }
- catch { case ERROR(_) => markup_malformed(source) }
- }
-}
--- a/src/Pure/IsaMakefile Mon Sep 05 19:18:38 2011 +0200
+++ b/src/Pure/IsaMakefile Tue Sep 06 07:23:45 2011 +0200
@@ -105,8 +105,6 @@
General/table.ML \
General/timing.ML \
General/url.ML \
- General/xml.ML \
- General/yxml.ML \
Isar/args.ML \
Isar/attrib.ML \
Isar/auto_bind.ML \
@@ -158,6 +156,8 @@
ML/ml_thms.ML \
PIDE/document.ML \
PIDE/isar_document.ML \
+ PIDE/xml.ML \
+ PIDE/yxml.ML \
Proof/extraction.ML \
Proof/proof_checker.ML \
Proof/proof_rewrite_rules.ML \
--- a/src/Pure/ML/ml_lex.ML Mon Sep 05 19:18:38 2011 +0200
+++ b/src/Pure/ML/ml_lex.ML Tue Sep 06 07:23:45 2011 +0200
@@ -106,8 +106,8 @@
val token_kind_markup =
fn Keyword => Markup.ML_keyword
- | Ident => Markup.ML_ident
- | LongIdent => Markup.ML_ident
+ | Ident => Markup.empty
+ | LongIdent => Markup.empty
| TypeVar => Markup.ML_tvar
| Word => Markup.ML_numeral
| Int => Markup.ML_numeral
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/xml.ML Tue Sep 06 07:23:45 2011 +0200
@@ -0,0 +1,363 @@
+(* Title: Pure/PIDE/xml.ML
+ Author: David Aspinall
+ Author: Stefan Berghofer
+ Author: Makarius
+
+Untyped XML trees and basic data representation.
+*)
+
+signature XML_DATA_OPS =
+sig
+ type 'a A
+ type 'a T
+ type 'a V
+ val int_atom: int A
+ val bool_atom: bool A
+ val unit_atom: unit A
+ val properties: Properties.T T
+ val string: string T
+ val int: int T
+ val bool: bool T
+ val unit: unit T
+ val pair: 'a T -> 'b T -> ('a * 'b) T
+ val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
+ val list: 'a T -> 'a list T
+ val option: 'a T -> 'a option T
+ val variant: 'a V list -> 'a T
+end;
+
+signature XML =
+sig
+ type attributes = Properties.T
+ datatype tree =
+ Elem of Markup.T * tree list
+ | Text of string
+ type body = tree list
+ val add_content: tree -> Buffer.T -> Buffer.T
+ val content_of: body -> string
+ val header: string
+ val text: string -> string
+ val element: string -> attributes -> string list -> string
+ val output_markup: Markup.T -> Output.output * Output.output
+ val string_of: tree -> string
+ val pretty: int -> tree -> Pretty.T
+ val output: tree -> TextIO.outstream -> unit
+ val parse_comments: string list -> unit * string list
+ val parse_string : string -> string option
+ val parse_element: string list -> tree * string list
+ val parse_document: string list -> tree * string list
+ val parse: string -> tree
+ exception XML_ATOM of string
+ exception XML_BODY of body
+ structure Encode: XML_DATA_OPS
+ structure Decode: XML_DATA_OPS
+end;
+
+structure XML: XML =
+struct
+
+(** XML trees **)
+
+type attributes = Properties.T;
+
+datatype tree =
+ Elem of Markup.T * tree list
+ | Text of string;
+
+type body = tree list;
+
+fun add_content (Elem (_, ts)) = fold add_content ts
+ | add_content (Text s) = Buffer.add s;
+
+fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
+
+
+
+(** string representation **)
+
+val header = "<?xml version=\"1.0\"?>\n";
+
+
+(* escaped text *)
+
+fun decode "<" = "<"
+ | decode ">" = ">"
+ | decode "&" = "&"
+ | decode "'" = "'"
+ | decode """ = "\""
+ | decode c = c;
+
+fun encode "<" = "<"
+ | encode ">" = ">"
+ | encode "&" = "&"
+ | encode "'" = "'"
+ | encode "\"" = """
+ | encode c = c;
+
+val text = translate_string encode;
+
+
+(* elements *)
+
+fun elem name atts =
+ space_implode " " (name :: map (fn (a, x) => a ^ "=\"" ^ text x ^ "\"") atts);
+
+fun element name atts body =
+ let val b = implode body in
+ if b = "" then enclose "<" "/>" (elem name atts)
+ else enclose "<" ">" (elem name atts) ^ b ^ enclose "</" ">" name
+ end;
+
+fun output_markup (markup as (name, atts)) =
+ if Markup.is_empty markup then Markup.no_output
+ else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
+
+
+(* output *)
+
+fun buffer_of depth tree =
+ let
+ fun traverse _ (Elem ((name, atts), [])) =
+ Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
+ | traverse d (Elem ((name, atts), ts)) =
+ Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
+ traverse_body d ts #>
+ Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
+ | traverse _ (Text s) = Buffer.add (text s)
+ and traverse_body 0 _ = Buffer.add "..."
+ | traverse_body d ts = fold (traverse (d - 1)) ts;
+ in Buffer.empty |> traverse depth tree end;
+
+val string_of = Buffer.content o buffer_of ~1;
+val output = Buffer.output o buffer_of ~1;
+
+fun pretty depth tree =
+ Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
+
+
+
+(** XML parsing **)
+
+local
+
+fun err msg (xs, _) =
+ fn () => "XML parsing error: " ^ msg () ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
+
+fun ignored _ = [];
+
+val blanks = Scan.many Symbol.is_blank;
+val special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
+val regular = Scan.one Symbol.is_regular;
+fun regular_except x = Scan.one (fn c => Symbol.is_regular c andalso c <> x);
+
+val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode;
+
+val parse_cdata =
+ Scan.this_string "<![CDATA[" |--
+ (Scan.repeat (Scan.unless (Scan.this_string "]]>") regular) >> implode) --|
+ Scan.this_string "]]>";
+
+val parse_att =
+ (Symbol.scan_id --| (blanks -- $$ "=" -- blanks)) --
+ (($$ "\"" || $$ "'") :|-- (fn s =>
+ (Scan.repeat (special || regular_except s) >> implode) --| $$ s));
+
+val parse_comment =
+ Scan.this_string "<!--" --
+ Scan.repeat (Scan.unless (Scan.this_string "-->") regular) --
+ Scan.this_string "-->" >> ignored;
+
+val parse_processing_instruction =
+ Scan.this_string "<?" --
+ Scan.repeat (Scan.unless (Scan.this_string "?>") regular) --
+ Scan.this_string "?>" >> ignored;
+
+val parse_doctype =
+ Scan.this_string "<!DOCTYPE" --
+ Scan.repeat (Scan.unless ($$ ">") regular) --
+ $$ ">" >> ignored;
+
+val parse_misc =
+ Scan.one Symbol.is_blank >> ignored ||
+ parse_processing_instruction ||
+ parse_comment;
+
+val parse_optional_text =
+ Scan.optional (parse_chars >> (single o Text)) [];
+
+fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_";
+fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = ".";
+val parse_name = Scan.one name_start_char ::: Scan.many name_char;
+
+in
+
+val parse_comments =
+ blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K ();
+
+val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode;
+
+fun parse_content xs =
+ (parse_optional_text @@@
+ (Scan.repeat
+ ((parse_element >> single ||
+ parse_cdata >> (single o Text) ||
+ parse_processing_instruction ||
+ parse_comment)
+ @@@ parse_optional_text) >> flat)) xs
+
+and parse_element xs =
+ ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--
+ (fn (name, _) =>
+ !! (err (fn () => "Expected > or />"))
+ ($$ "/" -- $$ ">" >> ignored ||
+ $$ ">" |-- parse_content --|
+ !! (err (fn () => "Expected </" ^ implode name ^ ">"))
+ ($$ "<" -- $$ "/" -- Scan.this name -- blanks -- $$ ">")))
+ >> (fn ((name, atts), body) => Elem ((implode name, atts), body))) xs;
+
+val parse_document =
+ (Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc)
+ |-- parse_element;
+
+fun parse s =
+ (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element"))
+ (blanks |-- parse_document --| blanks))) (raw_explode s) of
+ (x, []) => x
+ | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));
+
+end;
+
+
+
+(** XML as data representation language **)
+
+exception XML_ATOM of string;
+exception XML_BODY of tree list;
+
+
+structure Encode =
+struct
+
+type 'a A = 'a -> string;
+type 'a T = 'a -> body;
+type 'a V = 'a -> string list * body;
+
+
+(* atomic values *)
+
+fun int_atom i = signed_string_of_int i;
+
+fun bool_atom false = "0"
+ | bool_atom true = "1";
+
+fun unit_atom () = "";
+
+
+(* structural nodes *)
+
+fun node ts = Elem ((":", []), ts);
+
+fun vector xs = map_index (fn (i, x) => (int_atom i, x)) xs;
+
+fun tagged (tag, (xs, ts)) = Elem ((int_atom tag, vector xs), ts);
+
+
+(* representation of standard types *)
+
+fun properties props = [Elem ((":", props), [])];
+
+fun string "" = []
+ | string s = [Text s];
+
+val int = string o int_atom;
+
+val bool = string o bool_atom;
+
+val unit = string o unit_atom;
+
+fun pair f g (x, y) = [node (f x), node (g y)];
+
+fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
+
+fun list f xs = map (node o f) xs;
+
+fun option _ NONE = []
+ | option f (SOME x) = [node (f x)];
+
+fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
+
+end;
+
+
+structure Decode =
+struct
+
+type 'a A = string -> 'a;
+type 'a T = body -> 'a;
+type 'a V = string list * body -> 'a;
+
+
+(* atomic values *)
+
+fun int_atom s =
+ Markup.parse_int s
+ handle Fail _ => raise XML_ATOM s;
+
+fun bool_atom "0" = false
+ | bool_atom "1" = true
+ | bool_atom s = raise XML_ATOM s;
+
+fun unit_atom "" = ()
+ | unit_atom s = raise XML_ATOM s;
+
+
+(* structural nodes *)
+
+fun node (Elem ((":", []), ts)) = ts
+ | node t = raise XML_BODY [t];
+
+fun vector atts =
+ #1 (fold_map (fn (a, x) =>
+ fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts 0);
+
+fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
+ | tagged t = raise XML_BODY [t];
+
+
+(* representation of standard types *)
+
+fun properties [Elem ((":", props), [])] = props
+ | properties ts = raise XML_BODY ts;
+
+fun string [] = ""
+ | string [Text s] = s
+ | string ts = raise XML_BODY ts;
+
+val int = int_atom o string;
+
+val bool = bool_atom o string;
+
+val unit = unit_atom o string;
+
+fun pair f g [t1, t2] = (f (node t1), g (node t2))
+ | pair _ _ ts = raise XML_BODY ts;
+
+fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
+ | triple _ _ _ ts = raise XML_BODY ts;
+
+fun list f ts = map (f o node) ts;
+
+fun option _ [] = NONE
+ | option f [t] = SOME (f (node t))
+ | option _ ts = raise XML_BODY ts;
+
+fun variant fs [t] =
+ let
+ val (tag, (xs, ts)) = tagged t;
+ val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
+ in f (xs, ts) end
+ | variant _ ts = raise XML_BODY ts;
+
+end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/xml.scala Tue Sep 06 07:23:45 2011 +0200
@@ -0,0 +1,368 @@
+/* Title: Pure/PIDE/xml.scala
+ Author: Makarius
+
+Untyped XML trees and basic data representation.
+*/
+
+package isabelle
+
+import java.lang.System
+import java.util.WeakHashMap
+import java.lang.ref.WeakReference
+import javax.xml.parsers.DocumentBuilderFactory
+
+import scala.actors.Actor._
+import scala.collection.mutable
+
+
+object XML
+{
+ /** XML trees **/
+
+ /* datatype representation */
+
+ type Attributes = Properties.T
+
+ sealed abstract class Tree { override def toString = string_of_tree(this) }
+ case class Elem(markup: Markup, body: List[Tree]) extends Tree
+ case class Text(content: String) extends Tree
+
+ def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
+ def elem(name: String) = Elem(Markup(name, Nil), Nil)
+
+ type Body = List[Tree]
+
+
+ /* string representation */
+
+ def string_of_body(body: Body): String =
+ {
+ val s = new StringBuilder
+
+ def text(txt: String) {
+ if (txt == null) s ++= txt
+ else {
+ for (c <- txt.iterator) c match {
+ case '<' => s ++= "<"
+ case '>' => s ++= ">"
+ case '&' => s ++= "&"
+ case '"' => s ++= """
+ case '\'' => s ++= "'"
+ case _ => s += c
+ }
+ }
+ }
+ def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
+ def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
+ def tree(t: Tree): Unit =
+ t match {
+ case Elem(markup, Nil) =>
+ s ++= "<"; elem(markup); s ++= "/>"
+ case Elem(markup, ts) =>
+ s ++= "<"; elem(markup); s ++= ">"
+ ts.foreach(tree)
+ s ++= "</"; s ++= markup.name; s ++= ">"
+ case Text(txt) => text(txt)
+ }
+ body.foreach(tree)
+ s.toString
+ }
+
+ def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
+
+
+ /* text content */
+
+ def content_stream(tree: Tree): Stream[String] =
+ tree match {
+ case Elem(_, body) => content_stream(body)
+ case Text(content) => Stream(content)
+ }
+ def content_stream(body: Body): Stream[String] =
+ body.toStream.flatten(content_stream(_))
+
+ def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
+ def content(body: Body): Iterator[String] = content_stream(body).iterator
+
+
+ /* pipe-lined cache for partial sharing */
+
+ class Cache(initial_size: Int = 131071, max_string: Int = 100)
+ {
+ private var table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
+
+ private def lookup[A](x: A): Option[A] =
+ {
+ val ref = table.get(x)
+ if (ref == null) None
+ else {
+ val y = ref.asInstanceOf[WeakReference[A]].get
+ if (y == null) None
+ else Some(y)
+ }
+ }
+ private def store[A](x: A): A =
+ {
+ table.put(x, new WeakReference[Any](x))
+ x
+ }
+
+ private def trim_bytes(s: String): String = new String(s.toCharArray)
+
+ private def _cache_string(x: String): String =
+ lookup(x) match {
+ case Some(y) => y
+ case None =>
+ val z = trim_bytes(x)
+ if (z.length > max_string) z else store(z)
+ }
+ private def _cache_props(x: Properties.T): Properties.T =
+ if (x.isEmpty) x
+ else
+ lookup(x) match {
+ case Some(y) => y
+ case None => store(x.map(p => (trim_bytes(p._1).intern, _cache_string(p._2))))
+ }
+ private def _cache_markup(x: Markup): Markup =
+ lookup(x) match {
+ case Some(y) => y
+ case None =>
+ x match {
+ case Markup(name, props) =>
+ store(Markup(_cache_string(name), _cache_props(props)))
+ }
+ }
+ private def _cache_tree(x: XML.Tree): XML.Tree =
+ lookup(x) match {
+ case Some(y) => y
+ case None =>
+ x match {
+ case XML.Elem(markup, body) =>
+ store(XML.Elem(_cache_markup(markup), _cache_body(body)))
+ case XML.Text(text) => store(XML.Text(_cache_string(text)))
+ }
+ }
+ private def _cache_body(x: XML.Body): XML.Body =
+ if (x.isEmpty) x
+ else
+ lookup(x) match {
+ case Some(y) => y
+ case None => x.map(_cache_tree(_))
+ }
+
+ // main methods
+ def cache_string(x: String): String = synchronized { _cache_string(x) }
+ def cache_markup(x: Markup): Markup = synchronized { _cache_markup(x) }
+ def cache_tree(x: XML.Tree): XML.Tree = synchronized { _cache_tree(x) }
+ def cache_body(x: XML.Body): XML.Body = synchronized { _cache_body(x) }
+ }
+
+
+
+ /** document object model (W3C DOM) **/
+
+ def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
+ node.getUserData(Markup.Data.name) match {
+ case tree: XML.Tree => Some(tree)
+ case _ => None
+ }
+
+ def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
+ {
+ def DOM(tr: Tree): org.w3c.dom.Node = tr match {
+ case Elem(Markup.Data, List(data, t)) =>
+ val node = DOM(t)
+ node.setUserData(Markup.Data.name, data, null)
+ node
+ case Elem(Markup(name, atts), ts) =>
+ if (name == Markup.Data.name)
+ error("Malformed data element: " + tr.toString)
+ val node = doc.createElement(name)
+ for ((name, value) <- atts) node.setAttribute(name, value)
+ for (t <- ts) node.appendChild(DOM(t))
+ node
+ case Text(txt) => doc.createTextNode(txt)
+ }
+ DOM(tree)
+ }
+
+
+
+ /** XML as data representation language **/
+
+ class XML_Atom(s: String) extends Exception(s)
+ class XML_Body(body: XML.Body) extends Exception
+
+ object Encode
+ {
+ type T[A] = A => XML.Body
+
+
+ /* atomic values */
+
+ def long_atom(i: Long): String = i.toString
+
+ def int_atom(i: Int): String = i.toString
+
+ def bool_atom(b: Boolean): String = if (b) "1" else "0"
+
+ def unit_atom(u: Unit) = ""
+
+
+ /* structural nodes */
+
+ private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
+
+ private def vector(xs: List[String]): XML.Attributes =
+ xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
+
+ private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
+ XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
+
+
+ /* representation of standard types */
+
+ val properties: T[Properties.T] =
+ (props => List(XML.Elem(Markup(":", props), Nil)))
+
+ val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
+
+ val long: T[Long] = (x => string(long_atom(x)))
+
+ val int: T[Int] = (x => string(int_atom(x)))
+
+ val bool: T[Boolean] = (x => string(bool_atom(x)))
+
+ val unit: T[Unit] = (x => string(unit_atom(x)))
+
+ def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
+ (x => List(node(f(x._1)), node(g(x._2))))
+
+ def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
+ (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
+
+ def list[A](f: T[A]): T[List[A]] =
+ (xs => xs.map((x: A) => node(f(x))))
+
+ def option[A](f: T[A]): T[Option[A]] =
+ {
+ case None => Nil
+ case Some(x) => List(node(f(x)))
+ }
+
+ def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
+ {
+ case x =>
+ val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
+ List(tagged(tag, f(x)))
+ }
+ }
+
+ object Decode
+ {
+ type T[A] = XML.Body => A
+ type V[A] = (List[String], XML.Body) => A
+
+
+ /* atomic values */
+
+ def long_atom(s: String): Long =
+ try { java.lang.Long.parseLong(s) }
+ catch { case e: NumberFormatException => throw new XML_Atom(s) }
+
+ def int_atom(s: String): Int =
+ try { Integer.parseInt(s) }
+ catch { case e: NumberFormatException => throw new XML_Atom(s) }
+
+ def bool_atom(s: String): Boolean =
+ if (s == "1") true
+ else if (s == "0") false
+ else throw new XML_Atom(s)
+
+ def unit_atom(s: String): Unit =
+ if (s == "") () else throw new XML_Atom(s)
+
+
+ /* structural nodes */
+
+ private def node(t: XML.Tree): XML.Body =
+ t match {
+ case XML.Elem(Markup(":", Nil), ts) => ts
+ case _ => throw new XML_Body(List(t))
+ }
+
+ private def vector(atts: XML.Attributes): List[String] =
+ {
+ val xs = new mutable.ListBuffer[String]
+ var i = 0
+ for ((a, x) <- atts) {
+ if (int_atom(a) == i) { xs += x; i = i + 1 }
+ else throw new XML_Atom(a)
+ }
+ xs.toList
+ }
+
+ private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
+ t match {
+ case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
+ case _ => throw new XML_Body(List(t))
+ }
+
+
+ /* representation of standard types */
+
+ val properties: T[Properties.T] =
+ {
+ case List(XML.Elem(Markup(":", props), Nil)) => props
+ case ts => throw new XML_Body(ts)
+ }
+
+ val string: T[String] =
+ {
+ case Nil => ""
+ case List(XML.Text(s)) => s
+ case ts => throw new XML_Body(ts)
+ }
+
+ val long: T[Long] = (x => long_atom(string(x)))
+
+ val int: T[Int] = (x => int_atom(string(x)))
+
+ val bool: T[Boolean] = (x => bool_atom(string(x)))
+
+ val unit: T[Unit] = (x => unit_atom(string(x)))
+
+ def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
+ {
+ case List(t1, t2) => (f(node(t1)), g(node(t2)))
+ case ts => throw new XML_Body(ts)
+ }
+
+ def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
+ {
+ case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
+ case ts => throw new XML_Body(ts)
+ }
+
+ def list[A](f: T[A]): T[List[A]] =
+ (ts => ts.map(t => f(node(t))))
+
+ def option[A](f: T[A]): T[Option[A]] =
+ {
+ case Nil => None
+ case List(t) => Some(f(node(t)))
+ case ts => throw new XML_Body(ts)
+ }
+
+ def variant[A](fs: List[V[A]]): T[A] =
+ {
+ case List(t) =>
+ val (tag, (xs, ts)) = tagged(t)
+ val f =
+ try { fs(tag) }
+ catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
+ f(xs, ts)
+ case ts => throw new XML_Body(ts)
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/yxml.ML Tue Sep 06 07:23:45 2011 +0200
@@ -0,0 +1,148 @@
+(* Title: Pure/PIDE/yxml.ML
+ Author: Makarius
+
+Efficient text representation of XML trees using extra characters X
+and Y -- no escaping, may nest marked text verbatim. Suitable for
+direct inlining into plain text.
+
+Markup <elem att="val" ...>...body...</elem> is encoded as:
+
+ X Y name Y att=val ... X
+ ...
+ body
+ ...
+ X Y X
+*)
+
+signature YXML =
+sig
+ val X: Symbol.symbol
+ val Y: Symbol.symbol
+ val embed_controls: string -> string
+ val detect: string -> bool
+ val output_markup: Markup.T -> string * string
+ val element: string -> XML.attributes -> string list -> string
+ val string_of_body: XML.body -> string
+ val string_of: XML.tree -> string
+ val parse_body: string -> XML.body
+ val parse: string -> XML.tree
+end;
+
+structure YXML: YXML =
+struct
+
+(** string representation **)
+
+(* idempotent recoding of certain low ASCII control characters *)
+
+fun pseudo_utf8 c =
+ if Symbol.is_ascii_control c
+ then chr 192 ^ chr (128 + ord c)
+ else c;
+
+fun embed_controls str =
+ if exists_string Symbol.is_ascii_control str
+ then translate_string pseudo_utf8 str
+ else str;
+
+
+(* markers *)
+
+val X = chr 5;
+val Y = chr 6;
+val XY = X ^ Y;
+val XYX = XY ^ X;
+
+val detect = exists_string (fn s => s = X orelse s = Y);
+
+
+(* output *)
+
+fun output_markup (markup as (name, atts)) =
+ if Markup.is_empty markup then Markup.no_output
+ else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
+
+fun element name atts body =
+ let val (pre, post) = output_markup (name, atts)
+ in pre ^ implode body ^ post end;
+
+fun string_of_body body =
+ let
+ fun attrib (a, x) =
+ Buffer.add Y #>
+ Buffer.add a #> Buffer.add "=" #> Buffer.add x;
+ fun tree (XML.Elem ((name, atts), ts)) =
+ Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
+ trees ts #>
+ Buffer.add XYX
+ | tree (XML.Text s) = Buffer.add s
+ and trees ts = fold tree ts;
+ in Buffer.empty |> trees body |> Buffer.content end;
+
+val string_of = string_of_body o single;
+
+
+
+(** efficient YXML parsing **)
+
+local
+
+(* splitting *)
+
+fun is_char s c = ord s = Char.ord c;
+
+val split_string =
+ Substring.full #>
+ Substring.tokens (is_char X) #>
+ map (Substring.fields (is_char Y) #> map Substring.string);
+
+
+(* structural errors *)
+
+fun err msg = raise Fail ("Malformed YXML encoding: " ^ msg);
+fun err_attribute () = err "bad attribute";
+fun err_element () = err "bad element";
+fun err_unbalanced "" = err "unbalanced element"
+ | err_unbalanced name = err ("unbalanced element " ^ quote name);
+
+
+(* stack operations *)
+
+fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending;
+
+fun push "" _ _ = err_element ()
+ | push name atts pending = ((name, atts), []) :: pending;
+
+fun pop ((("", _), _) :: _) = err_unbalanced ""
+ | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
+
+
+(* parsing *)
+
+fun parse_attrib s =
+ (case first_field "=" s of
+ NONE => err_attribute ()
+ | SOME ("", _) => err_attribute ()
+ | SOME att => att);
+
+fun parse_chunk ["", ""] = pop
+ | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
+ | parse_chunk txts = fold (add o XML.Text) txts;
+
+in
+
+fun parse_body source =
+ (case fold parse_chunk (split_string source) [(("", []), [])] of
+ [(("", _), result)] => rev result
+ | ((name, _), _) :: _ => err_unbalanced name);
+
+fun parse source =
+ (case parse_body source of
+ [result] => result
+ | [] => XML.Text ""
+ | _ => err "multiple results");
+
+end;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/yxml.scala Tue Sep 06 07:23:45 2011 +0200
@@ -0,0 +1,135 @@
+/* Title: Pure/PIDE/yxml.scala
+ Author: Makarius
+
+Efficient text representation of XML trees. Suitable for direct
+inlining into plain text.
+*/
+
+package isabelle
+
+
+import scala.collection.mutable
+
+
+object YXML
+{
+ /* chunk markers */
+
+ val X = '\5'
+ val Y = '\6'
+ val X_string = X.toString
+ val Y_string = Y.toString
+
+ def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
+
+
+ /* string representation */ // FIXME byte array version with pseudo-utf-8 (!?)
+
+ def string_of_body(body: XML.Body): String =
+ {
+ val s = new StringBuilder
+ def attrib(p: (String, String)) { s += Y; s ++= p._1; s += '='; s ++= p._2 }
+ def tree(t: XML.Tree): Unit =
+ t match {
+ case XML.Elem(Markup(name, atts), ts) =>
+ s += X; s += Y; s++= name; atts.foreach(attrib); s += X
+ ts.foreach(tree)
+ s += X; s += Y; s += X
+ case XML.Text(text) => s ++= text
+ }
+ body.foreach(tree)
+ s.toString
+ }
+
+ def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
+
+
+ /* parsing */
+
+ private def err(msg: String) = error("Malformed YXML: " + msg)
+ private def err_attribute() = err("bad attribute")
+ private def err_element() = err("bad element")
+ private def err_unbalanced(name: String) =
+ if (name == "") err("unbalanced element")
+ else err("unbalanced element " + quote(name))
+
+ private def parse_attrib(source: CharSequence) = {
+ val s = source.toString
+ val i = s.indexOf('=')
+ if (i <= 0) err_attribute()
+ (s.substring(0, i), s.substring(i + 1))
+ }
+
+
+ def parse_body(source: CharSequence): XML.Body =
+ {
+ /* stack operations */
+
+ def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
+ var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
+
+ def add(x: XML.Tree)
+ {
+ (stack: @unchecked) match { case ((_, body) :: _) => body += x }
+ }
+
+ def push(name: String, atts: XML.Attributes)
+ {
+ if (name == "") err_element()
+ else stack = (Markup(name, atts), buffer()) :: stack
+ }
+
+ def pop()
+ {
+ (stack: @unchecked) match {
+ case ((Markup.Empty, _) :: _) => err_unbalanced("")
+ case ((markup, body) :: pending) =>
+ stack = pending
+ add(XML.Elem(markup, body.toList))
+ }
+ }
+
+
+ /* parse chunks */
+
+ for (chunk <- Library.chunks(source, X) if chunk.length != 0) {
+ if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
+ else {
+ Library.chunks(chunk, Y).toList match {
+ case ch :: name :: atts if ch.length == 0 =>
+ push(name.toString, atts.map(parse_attrib))
+ case txts => for (txt <- txts) add(XML.Text(txt.toString))
+ }
+ }
+ }
+ (stack: @unchecked) match {
+ case List((Markup.Empty, body)) => body.toList
+ case (Markup(name, _), _) :: _ => err_unbalanced(name)
+ }
+ }
+
+ def parse(source: CharSequence): XML.Tree =
+ parse_body(source) match {
+ case List(result) => result
+ case Nil => XML.Text("")
+ case _ => err("multiple results")
+ }
+
+
+ /* failsafe parsing */
+
+ private def markup_malformed(source: CharSequence) =
+ XML.elem(Markup.MALFORMED, List(XML.Text(source.toString)))
+
+ def parse_body_failsafe(source: CharSequence): XML.Body =
+ {
+ try { parse_body(source) }
+ catch { case ERROR(_) => List(markup_malformed(source)) }
+ }
+
+ def parse_failsafe(source: CharSequence): XML.Tree =
+ {
+ try { parse(source) }
+ catch { case ERROR(_) => markup_malformed(source) }
+ }
+}
--- a/src/Pure/ROOT.ML Mon Sep 05 19:18:38 2011 +0200
+++ b/src/Pure/ROOT.ML Tue Sep 06 07:23:45 2011 +0200
@@ -54,17 +54,18 @@
use "General/linear_set.ML";
use "General/buffer.ML";
use "General/pretty.ML";
-use "General/xml.ML";
use "General/path.ML";
use "General/url.ML";
use "General/file.ML";
-use "General/yxml.ML";
use "General/long_name.ML";
use "General/binding.ML";
use "General/sha1.ML";
if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
+use "PIDE/xml.ML";
+use "PIDE/yxml.ML";
+
(* concurrency within the ML runtime *)
--- a/src/Pure/Syntax/lexicon.ML Mon Sep 05 19:18:38 2011 +0200
+++ b/src/Pure/Syntax/lexicon.ML Tue Sep 06 07:23:45 2011 +0200
@@ -190,8 +190,8 @@
val token_kind_markup =
fn Literal => Markup.literal
- | IdentSy => Markup.ident
- | LongIdentSy => Markup.ident
+ | IdentSy => Markup.empty
+ | LongIdentSy => Markup.empty
| VarSy => Markup.var
| TFreeSy => Markup.tfree
| TVarSy => Markup.tvar
--- a/src/Pure/System/isabelle_process.scala Mon Sep 05 19:18:38 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala Tue Sep 06 07:23:45 2011 +0200
@@ -99,12 +99,10 @@
{
if (kind == Markup.INIT) rm_fifos()
if (kind == Markup.RAW)
- xml_cache.cache_ignore(
- new Result(XML.Elem(Markup(kind, props), body)))((result: Result) => receiver ! result)
+ receiver ! new Result(XML.Elem(Markup(kind, props), body))
else {
val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
- xml_cache.cache_tree(msg)((message: XML.Tree) =>
- receiver ! new Result(message.asInstanceOf[XML.Elem]))
+ receiver ! new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem])
}
}
--- a/src/Pure/Thy/thy_syntax.ML Mon Sep 05 19:18:38 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Tue Sep 06 07:23:45 2011 +0200
@@ -45,14 +45,14 @@
val token_kind_markup =
fn Token.Command => Markup.command
| Token.Keyword => Markup.keyword
- | Token.Ident => Markup.ident
- | Token.LongIdent => Markup.ident
- | Token.SymIdent => Markup.ident
+ | Token.Ident => Markup.empty
+ | Token.LongIdent => Markup.empty
+ | Token.SymIdent => Markup.empty
| Token.Var => Markup.var
| Token.TypeIdent => Markup.tfree
| Token.TypeVar => Markup.tvar
- | Token.Nat => Markup.ident
- | Token.Float => Markup.ident
+ | Token.Nat => Markup.empty
+ | Token.Float => Markup.empty
| Token.String => Markup.string
| Token.AltString => Markup.altstring
| Token.Verbatim => Markup.verbatim
--- a/src/Pure/build-jars Mon Sep 05 19:18:38 2011 +0200
+++ b/src/Pure/build-jars Tue Sep 06 07:23:45 2011 +0200
@@ -24,8 +24,6 @@
General/scan.scala
General/sha1.scala
General/symbol.scala
- General/xml.scala
- General/yxml.scala
Isar/keyword.scala
Isar/outer_syntax.scala
Isar/parse.scala
@@ -36,6 +34,8 @@
PIDE/isar_document.scala
PIDE/markup_tree.scala
PIDE/text.scala
+ PIDE/xml.scala
+ PIDE/yxml.scala
System/cygwin.scala
System/download.scala
System/event_bus.scala
--- a/src/Tools/jEdit/README Mon Sep 05 19:18:38 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,62 +0,0 @@
-Isabelle/jEdit based on Isabelle/Scala
-======================================
-
-The Isabelle/Scala layer that is already part of Isabelle/Pure
-provides some general infrastructure for advanced prover interaction
-and integration. The Isabelle/jEdit application serves as an example
-for asynchronous proof checking with support for parallel processing.
-
-See also the paper:
-
- Makarius Wenzel. Asynchronous Proof Processing with Isabelle/Scala
- and Isabelle/jEdit. In C. Sacerdoti Coen and D. Aspinall, editors,
- User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite
- Workshop, Edinburgh, Scotland, July 2010. To appear in ENTCS.
- http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf
-
-
-Known problems with Mac OS
-==========================
-
-- The MacOSX plugin for jEdit disrupts regular C-X/C/V operations,
- e.g. between the editor and the Console plugin, which is a standard
- swing text box. Similar for search boxes etc.
-
-- ToggleButton selected state is not rendered if window focus is lost,
- which is probably a genuine feature of the Apple look-and-feel.
-
-- Anti-aliasing does not really work as well as for Linux or Windows.
- (General Apple/Swing problem?)
-
-- Font.createFont mangles the font family of non-regular fonts,
- e.g. bold. IsabelleText font files need to be installed manually.
-
-- Missing glyphs are collected from other fonts (like Emacs, Firefox).
- This is actually an advantage over the Oracle/Sun JVM on Windows or
- Linux, but probably also the deeper reason for the other oddities of
- Apple font management.
-
-- The native font renderer of -Dapple.awt.graphics.UseQuartz=true
- fails to handle the infinitesimal font size of "hidden" text (e.g.
- used in Isabelle sub/superscripts).
-
-
-Known problems with OpenJDK
-===========================
-
-- The 2D rendering engine of OpenJDK 1.6.x distorts the appearance of
- the jEdit text area. Always use official JRE 1.6.x from
- Sun/Oracle/Apple.
-
-
-Licenses and home sites of contributing systems
-===============================================
-
-* Scala: BSD-style
- http://www.scala-lang.org
-
-* jEdit: GPL (with special cases)
- http://www.jedit.org/
-
-* Lobo/Cobra: GPL and LGPL
- http://lobobrowser.org/
--- a/src/Tools/jEdit/README.html Mon Sep 05 19:18:38 2011 +0200
+++ b/src/Tools/jEdit/README.html Tue Sep 06 07:23:45 2011 +0200
@@ -12,7 +12,12 @@
<body>
-<h2>The Isabelle/jEdit Prover IDE</h2>
+<h2>The Isabelle/jEdit Prover IDE (based on Isabelle/Scala)</h2>
+
+The Isabelle/Scala layer that is already part of Isabelle/Pure
+provides some general infrastructure for advanced prover interaction
+and integration. The Isabelle/jEdit application serves as an example
+for asynchronous proof checking with support for parallel processing.
<ul>
@@ -116,30 +121,23 @@
</ul>
-<h2>Limitations and workrounds (January 2011)</h2>
+<h2>Limitations and workrounds (September 2011)</h2>
<ul>
<li>No way to start/stop prover or switch to a different logic.<br/>
<em>Workaround:</em> Change options and restart editor.</li>
- <li>Limited support for dependencies between multiple theory buffers.<br/>
- <em>Workaround:</em> Load required files manually.</li>
-
- <li>No reclaiming of old/unused document versions in prover or
- editor.<br/>
- <em>Workaround:</em> Avoid large files; restart after a few hours of use.</li>
-
<li>Incremental reparsing sometimes produces unexpected command
spans.<br/>
<em>Workaround:</em> Cut/paste larger parts or reload buffer.</li>
- <li>Command execution sometimes gets stuck (purple background).<br/>
- <em>Workaround:</em> Force reparsing as above.</li>
+ <li>Odd behavior of some diagnostic commands, notably those starting
+ external processes asynchronously (e.g. <tt>thy_deps</tt>).<br/>
+ <em>Workaround:</em> Avoid such commands.</li>
- <li>Odd behavior of some diagnostic commands, notably those
- starting external processes asynchronously
- (e.g. <tt>thy_deps</tt>, <tt>sledgehammer</tt>).<br/>
- <em>Workaround:</em> Avoid such commands.</li>
+ <li>Lack of dependency managed for auxiliary files that contribute
+ to a theory ("<b>uses</b>").<br/>
+ <em>Workaround:</em> Re-use files manually within the prover.</li>
<li>No support for non-local markup, e.g. commands reporting on
previous commands (proof end on proof head), or markup produced by
@@ -149,6 +147,59 @@
General.</li>
</ul>
+
+<h2>Known problems with Mac OS</h2>
+
+<ul>
+
+<li>The MacOSX plugin for jEdit disrupts regular C-X/C/V operations,
+ e.g. between the editor and the Console plugin, which is a standard
+ swing text box. Similar for search boxes etc.</li>
+
+<li>ToggleButton selected state is not rendered if window focus is
+ lost, which is probably a genuine feature of the Apple
+ look-and-feel.</li>
+
+<li>Font.createFont mangles the font family of non-regular fonts,
+ e.g. bold. IsabelleText font files need to be installed/updated
+ manually.</li>
+
+<li>Missing glyphs are collected from other fonts (like Emacs,
+ Firefox). This is actually an advantage over the Oracle/Sun JVM on
+ Windows or Linux, but probably also the deeper reason for the other
+ oddities of Apple font management.</li>
+
+<li>The native font renderer of -Dapple.awt.graphics.UseQuartz=true
+ (not enabled by default) fails to handle the infinitesimal font size
+ of "hidden" text (e.g. used in Isabelle sub/superscripts).</li>
+
+</ul>
+
+
+<h2>Known problems with OpenJDK 1.6.x</h2>
+
+<ul>
+
+<li>The 2D rendering engine of OpenJDK 1.6.x distorts the appearance
+ of the jEdit text area. Always use official JRE 1.6.x from
+ Sun/Oracle/Apple.</li>
+
+<li>jEdit on OpenJDK is generally not supported.</li>
+
+</ul>
+
+
+<h2>Licenses and home sites of contributing systems</h2>
+
+<ul>
+
+<li>Scala: BSD-style <br/> http://www.scala-lang.org</li>
+
+<li>jEdit: GPL (with special cases) <br/> http://www.jedit.org/</li>
+
+<li>Lobo/Cobra: GPL and LGPL <br/> http://lobobrowser.org/</li>
+
+</ul>
+
</body>
</html>
-
--- a/src/Tools/jEdit/README_BUILD Mon Sep 05 19:18:38 2011 +0200
+++ b/src/Tools/jEdit/README_BUILD Tue Sep 06 07:23:45 2011 +0200
@@ -1,14 +1,14 @@
Requirements for instantaneous build from sources
=================================================
-* Official Java JDK from Sun/Oracle/Apple, e.g. 1.6.0_26
- http://java.sun.com/javase/downloads/index.jsp
+* Official Java JDK from Sun/Oracle/Apple, e.g. 1.6.0_27
+ http://www.oracle.com/technetwork/java/javase/downloads/index.html
* Scala Compiler 2.8.1.final
http://www.scala-lang.org
* Auxiliary jedit_build component
- http://www4.in.tum.de/~wenzelm/test/jedit_build-20110521.tar.gz
+ http://www4.in.tum.de/~wenzelm/test/jedit_build-20110622.tar.gz
Important settings within Isabelle environment
@@ -16,7 +16,7 @@
- JAVA_HOME
- SCALA_HOME
-- JEDIT_BUILD_HOME (via "init_component .../jedit_build...")
+- ISABELLE_JEDIT_BUILD_HOME (via "init_component .../jedit_build...")
Build and run
--- a/src/Tools/jEdit/src/isabelle_markup.scala Mon Sep 05 19:18:38 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala Tue Sep 06 07:23:45 2011 +0200
@@ -128,10 +128,7 @@
}
private val text_entity_colors: Map[String, Color] =
- Map(
- Markup.CLASS -> get_color("red"),
- Markup.TYPE -> get_color("black"),
- Markup.CONSTANT -> get_color("black"))
+ Map(Markup.CLASS -> get_color("red"))
private val text_colors: Map[String, Color] =
Map(
@@ -140,7 +137,6 @@
Markup.VERBATIM -> get_color("black"),
Markup.LITERAL -> keyword1_color,
Markup.DELIMITER -> get_color("black"),
- Markup.IDENT -> get_color("black"),
Markup.TFREE -> get_color("#A020F0"),
Markup.TVAR -> get_color("#A020F0"),
Markup.FREE -> get_color("blue"),
--- a/src/Tools/jEdit/src/isabelle_options.scala Mon Sep 05 19:18:38 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala Tue Sep 06 07:23:45 2011 +0200
@@ -63,6 +63,6 @@
tooltip_margin.getValue().asInstanceOf[Int]
Isabelle.Time_Property("tooltip-dismiss-delay") =
- Time.seconds(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
+ Time.ms(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
}
}
--- a/src/Tools/jEdit/src/plugin.scala Mon Sep 05 19:18:38 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Tue Sep 06 07:23:45 2011 +0200
@@ -123,8 +123,10 @@
Int_Property("tooltip-font-size", 10).toString + "px; \">" + // FIXME proper scaling (!?)
HTML.encode(text) + "</pre></html>"
+ private val tooltip_lb = Time.seconds(0.5)
+ private val tooltip_ub = Time.seconds(60.0)
def tooltip_dismiss_delay(): Time =
- Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5)
+ Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max tooltip_lb min tooltip_ub
def setup_tooltips()
{
--- a/src/Tools/jEdit/src/token_markup.scala Mon Sep 05 19:18:38 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Tue Sep 06 07:23:45 2011 +0200
@@ -173,41 +173,42 @@
case _ => Some(Scan.Finished)
}
val context1 =
- if (line_ctxt.isDefined && Isabelle.session.is_ready) {
- val syntax = Isabelle.session.current_syntax()
-
- val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
- val context1 = new Line_Context(Some(ctxt1))
-
- val extended = extended_styles(line)
-
- var offset = 0
- for (token <- tokens) {
- val style = Isabelle_Markup.token_markup(syntax, token)
- val length = token.source.length
- val end_offset = offset + length
- if ((offset until end_offset) exists extended.isDefinedAt) {
- for (i <- offset until end_offset) {
- val style1 =
- extended.get(i) match {
- case None => style
- case Some(ext) => ext(style)
- }
- handler.handleToken(line, style1, i, 1, context1)
- }
+ {
+ val (styled_tokens, context1) =
+ if (line_ctxt.isDefined && Isabelle.session.is_ready) {
+ val syntax = Isabelle.session.current_syntax()
+ val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
+ val styled_tokens = tokens.map(tok => (Isabelle_Markup.token_markup(syntax, tok), tok))
+ (styled_tokens, new Line_Context(Some(ctxt1)))
+ }
+ else {
+ val token = Token(Token.Kind.UNPARSED, line.subSequence(0, line.count).toString)
+ (List((JEditToken.NULL, token)), new Line_Context(None))
+ }
+
+ val extended = extended_styles(line)
+
+ var offset = 0
+ for ((style, token) <- styled_tokens) {
+ val length = token.source.length
+ val end_offset = offset + length
+ if ((offset until end_offset) exists
+ (i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {
+ for (i <- offset until end_offset) {
+ val style1 =
+ extended.get(i) match {
+ case None => style
+ case Some(ext) => ext(style)
+ }
+ handler.handleToken(line, style1, i, 1, context1)
}
- else handler.handleToken(line, style, offset, length, context1)
- offset += length
}
- handler.handleToken(line, JEditToken.END, line.count, 0, context1)
- context1
+ else handler.handleToken(line, style, offset, length, context1)
+ offset += length
}
- else {
- val context1 = new Line_Context(None)
- handler.handleToken(line, JEditToken.NULL, 0, line.count, context1)
- handler.handleToken(line, JEditToken.END, line.count, 0, context1)
- context1
- }
+ handler.handleToken(line, JEditToken.END, line.count, 0, context1)
+ context1
+ }
val context2 = context1.intern
handler.setLineContext(context2)
context2