merged
authorhaftmann
Tue Sep 06 07:23:45 2011 +0200 (2011-09-06)
changeset 44834242348d1b6d3
parent 44832 27fb2285bdee
parent 44833 9c6bd6204143
child 44835 ff6b9eb9c5ef
merged
src/Pure/General/xml.ML
src/Pure/General/xml.scala
src/Pure/General/yxml.ML
src/Pure/General/yxml.scala
src/Tools/jEdit/README
     1.1 --- a/NEWS	Mon Sep 05 19:18:38 2011 +0200
     1.2 +++ b/NEWS	Tue Sep 06 07:23:45 2011 +0200
     1.3 @@ -277,6 +277,8 @@
     1.4    realpow_two_diff ~> square_diff_square_factored
     1.5    reals_complete2 ~> complete_real
     1.6    exp_ln_eq ~> ln_unique
     1.7 +  expi_add ~> exp_add
     1.8 +  expi_zero ~> exp_zero
     1.9    lemma_DERIV_subst ~> DERIV_cong
    1.10    LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff
    1.11    LIMSEQ_const ~> tendsto_const
    1.12 @@ -296,6 +298,9 @@
    1.13    LIMSEQ_norm_zero ~> tendsto_norm_zero_iff
    1.14    LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff
    1.15    LIMSEQ_imp_rabs ~> tendsto_rabs
    1.16 +  LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus]
    1.17 +  LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const]
    1.18 +  LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const]
    1.19    LIM_ident ~> tendsto_ident_at
    1.20    LIM_const ~> tendsto_const
    1.21    LIM_add ~> tendsto_add
     2.1 --- a/etc/isabelle.css	Mon Sep 05 19:18:38 2011 +0200
     2.2 +++ b/etc/isabelle.css	Tue Sep 06 07:23:45 2011 +0200
     2.3 @@ -40,7 +40,6 @@
     2.4  .keyword        { font-weight: bold; }
     2.5  .operator       { }
     2.6  .command        { font-weight: bold; }
     2.7 -.ident          { }
     2.8  .string         { color: #008B00; }
     2.9  .altstring      { color: #8B8B00; }
    2.10  .verbatim       { color: #00008B; }
     3.1 --- a/src/HOL/Complex.thy	Mon Sep 05 19:18:38 2011 +0200
     3.2 +++ b/src/HOL/Complex.thy	Tue Sep 06 07:23:45 2011 +0200
     3.3 @@ -592,21 +592,20 @@
     3.4  
     3.5  subsection{*Finally! Polar Form for Complex Numbers*}
     3.6  
     3.7 -definition
     3.8 +text {* An abbreviation for @{text "cos a + i sin a"}. *}
     3.9  
    3.10 -  (* abbreviation for (cos a + i sin a) *)
    3.11 -  cis :: "real => complex" where
    3.12 +definition cis :: "real \<Rightarrow> complex" where
    3.13    "cis a = Complex (cos a) (sin a)"
    3.14  
    3.15 -definition
    3.16 -  (* abbreviation for r*(cos a + i sin a) *)
    3.17 -  rcis :: "[real, real] => complex" where
    3.18 +text {* An abbreviation for @{text "r(cos a + i sin a)"}. *}
    3.19 +
    3.20 +definition rcis :: "[real, real] \<Rightarrow> complex" where
    3.21    "rcis r a = complex_of_real r * cis a"
    3.22  
    3.23  abbreviation expi :: "complex \<Rightarrow> complex"
    3.24    where "expi \<equiv> exp"
    3.25  
    3.26 -lemma expi_imaginary: "expi (Complex 0 b) = cis b"
    3.27 +lemma cis_conv_exp: "cis b = exp (Complex 0 b)"
    3.28  proof (rule complex_eqI)
    3.29    { fix n have "Complex 0 b ^ n =
    3.30      real (fact n) *\<^sub>R Complex (cos_coeff n * b ^ n) (sin_coeff n * b ^ n)"
    3.31 @@ -614,23 +613,18 @@
    3.32        apply (simp add: cos_coeff_def sin_coeff_def)
    3.33        apply (simp add: sin_coeff_Suc cos_coeff_Suc del: mult_Suc)
    3.34        done } note * = this
    3.35 -  show "Re (exp (Complex 0 b)) = Re (cis b)"
    3.36 +  show "Re (cis b) = Re (exp (Complex 0 b))"
    3.37      unfolding exp_def cis_def cos_def
    3.38      by (subst bounded_linear.suminf[OF bounded_linear_Re summable_exp_generic],
    3.39        simp add: * mult_assoc [symmetric])
    3.40 -  show "Im (exp (Complex 0 b)) = Im (cis b)"
    3.41 +  show "Im (cis b) = Im (exp (Complex 0 b))"
    3.42      unfolding exp_def cis_def sin_def
    3.43      by (subst bounded_linear.suminf[OF bounded_linear_Im summable_exp_generic],
    3.44        simp add: * mult_assoc [symmetric])
    3.45  qed
    3.46  
    3.47  lemma expi_def: "expi z = complex_of_real (exp (Re z)) * cis (Im z)"
    3.48 -proof -
    3.49 -  have "expi z = expi (complex_of_real (Re z) + Complex 0 (Im z))"
    3.50 -    by simp
    3.51 -  thus ?thesis
    3.52 -    unfolding exp_add exp_of_real expi_imaginary .
    3.53 -qed
    3.54 +  unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by simp
    3.55  
    3.56  lemma complex_split_polar:
    3.57       "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
    3.58 @@ -665,11 +659,6 @@
    3.59  lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
    3.60  by simp
    3.61  
    3.62 -
    3.63 -(*---------------------------------------------------------------------------*)
    3.64 -(*  (r1 * cis a) * (r2 * cis b) = r1 * r2 * cis (a + b)                      *)
    3.65 -(*---------------------------------------------------------------------------*)
    3.66 -
    3.67  lemma cis_rcis_eq: "cis a = rcis 1 a"
    3.68  by (simp add: rcis_def)
    3.69  
    3.70 @@ -736,12 +725,6 @@
    3.71  lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
    3.72  by (auto simp add: DeMoivre)
    3.73  
    3.74 -lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
    3.75 -  by (rule exp_add) (* FIXME: redundant *)
    3.76 -
    3.77 -lemma expi_zero: "expi (0::complex) = 1"
    3.78 -  by (rule exp_zero) (* FIXME: redundant *)
    3.79 -
    3.80  lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
    3.81  apply (insert rcis_Ex [of z])
    3.82  apply (auto simp add: expi_def rcis_def mult_assoc [symmetric])
     4.1 --- a/src/HOL/Int.thy	Mon Sep 05 19:18:38 2011 +0200
     4.2 +++ b/src/HOL/Int.thy	Tue Sep 06 07:23:45 2011 +0200
     4.3 @@ -162,7 +162,10 @@
     4.4      by (simp add: Zero_int_def One_int_def)
     4.5  qed
     4.6  
     4.7 -lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
     4.8 +abbreviation int :: "nat \<Rightarrow> int" where
     4.9 +  "int \<equiv> of_nat"
    4.10 +
    4.11 +lemma int_def: "int m = Abs_Integ (intrel `` {(m, 0)})"
    4.12  by (induct m) (simp_all add: Zero_int_def One_int_def add)
    4.13  
    4.14  
    4.15 @@ -218,7 +221,7 @@
    4.16  
    4.17  text{*strict, in 1st argument; proof is by induction on k>0*}
    4.18  lemma zmult_zless_mono2_lemma:
    4.19 -     "(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j"
    4.20 +     "(i::int)<j ==> 0<k ==> int k * i < int k * j"
    4.21  apply (induct k)
    4.22  apply simp
    4.23  apply (simp add: left_distrib)
    4.24 @@ -226,13 +229,13 @@
    4.25  apply (simp_all add: add_strict_mono)
    4.26  done
    4.27  
    4.28 -lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
    4.29 +lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = int n"
    4.30  apply (cases k)
    4.31  apply (auto simp add: le add int_def Zero_int_def)
    4.32  apply (rule_tac x="x-y" in exI, simp)
    4.33  done
    4.34  
    4.35 -lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
    4.36 +lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = int n"
    4.37  apply (cases k)
    4.38  apply (simp add: less int_def Zero_int_def)
    4.39  apply (rule_tac x="x-y" in exI, simp)
    4.40 @@ -261,7 +264,7 @@
    4.41  done
    4.42  
    4.43  lemma zless_iff_Suc_zadd:
    4.44 -  "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + of_nat (Suc n))"
    4.45 +  "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
    4.46  apply (cases z, cases w)
    4.47  apply (auto simp add: less add int_def)
    4.48  apply (rename_tac a b c d) 
    4.49 @@ -314,7 +317,7 @@
    4.50  done
    4.51  
    4.52  text{*Collapse nested embeddings*}
    4.53 -lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
    4.54 +lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
    4.55  by (induct n) auto
    4.56  
    4.57  lemma of_int_power:
    4.58 @@ -400,13 +403,13 @@
    4.59      by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
    4.60  qed
    4.61  
    4.62 -lemma nat_int [simp]: "nat (of_nat n) = n"
    4.63 +lemma nat_int [simp]: "nat (int n) = n"
    4.64  by (simp add: nat int_def)
    4.65  
    4.66 -lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)"
    4.67 +lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
    4.68  by (cases z) (simp add: nat le int_def Zero_int_def)
    4.69  
    4.70 -corollary nat_0_le: "0 \<le> z ==> of_nat (nat z) = z"
    4.71 +corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
    4.72  by simp
    4.73  
    4.74  lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
    4.75 @@ -431,14 +434,14 @@
    4.76  
    4.77  lemma nonneg_eq_int:
    4.78    fixes z :: int
    4.79 -  assumes "0 \<le> z" and "\<And>m. z = of_nat m \<Longrightarrow> P"
    4.80 +  assumes "0 \<le> z" and "\<And>m. z = int m \<Longrightarrow> P"
    4.81    shows P
    4.82    using assms by (blast dest: nat_0_le sym)
    4.83  
    4.84 -lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)"
    4.85 +lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
    4.86  by (cases w) (simp add: nat le int_def Zero_int_def, arith)
    4.87  
    4.88 -corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)"
    4.89 +corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
    4.90  by (simp only: eq_commute [of m] nat_eq_iff)
    4.91  
    4.92  lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
    4.93 @@ -446,7 +449,7 @@
    4.94  apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith)
    4.95  done
    4.96  
    4.97 -lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> of_nat n"
    4.98 +lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
    4.99    by (cases x, simp add: nat le int_def le_diff_conv)
   4.100  
   4.101  lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
   4.102 @@ -470,10 +473,10 @@
   4.103  by (cases z, cases z')
   4.104    (simp add: nat add minus diff_minus le Zero_int_def)
   4.105  
   4.106 -lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0"
   4.107 +lemma nat_zminus_int [simp]: "nat (- int n) = 0"
   4.108  by (simp add: int_def minus nat Zero_int_def) 
   4.109  
   4.110 -lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)"
   4.111 +lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   4.112  by (cases z) (simp add: nat less int_def, arith)
   4.113  
   4.114  context ring_1
   4.115 @@ -491,31 +494,31 @@
   4.116  
   4.117  subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
   4.118  
   4.119 -lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \<Colon> int)"
   4.120 +lemma negative_zless_0: "- (int (Suc n)) < (0 \<Colon> int)"
   4.121  by (simp add: order_less_le del: of_nat_Suc)
   4.122  
   4.123 -lemma negative_zless [iff]: "- (of_nat (Suc n)) < (of_nat m \<Colon> int)"
   4.124 +lemma negative_zless [iff]: "- (int (Suc n)) < int m"
   4.125  by (rule negative_zless_0 [THEN order_less_le_trans], simp)
   4.126  
   4.127 -lemma negative_zle_0: "- of_nat n \<le> (0 \<Colon> int)"
   4.128 +lemma negative_zle_0: "- int n \<le> 0"
   4.129  by (simp add: minus_le_iff)
   4.130  
   4.131 -lemma negative_zle [iff]: "- of_nat n \<le> (of_nat m \<Colon> int)"
   4.132 +lemma negative_zle [iff]: "- int n \<le> int m"
   4.133  by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
   4.134  
   4.135 -lemma not_zle_0_negative [simp]: "~ (0 \<le> - (of_nat (Suc n) \<Colon> int))"
   4.136 +lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
   4.137  by (subst le_minus_iff, simp del: of_nat_Suc)
   4.138  
   4.139 -lemma int_zle_neg: "((of_nat n \<Colon> int) \<le> - of_nat m) = (n = 0 & m = 0)"
   4.140 +lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
   4.141  by (simp add: int_def le minus Zero_int_def)
   4.142  
   4.143 -lemma not_int_zless_negative [simp]: "~ ((of_nat n \<Colon> int) < - of_nat m)"
   4.144 +lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
   4.145  by (simp add: linorder_not_less)
   4.146  
   4.147 -lemma negative_eq_positive [simp]: "((- of_nat n \<Colon> int) = of_nat m) = (n = 0 & m = 0)"
   4.148 +lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)"
   4.149  by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
   4.150  
   4.151 -lemma zle_iff_zadd: "(w\<Colon>int) \<le> z \<longleftrightarrow> (\<exists>n. z = w + of_nat n)"
   4.152 +lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)"
   4.153  proof -
   4.154    have "(w \<le> z) = (0 \<le> z - w)"
   4.155      by (simp only: le_diff_eq add_0_left)
   4.156 @@ -526,10 +529,10 @@
   4.157    finally show ?thesis .
   4.158  qed
   4.159  
   4.160 -lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\<Colon>int)"
   4.161 +lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
   4.162  by simp
   4.163  
   4.164 -lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\<Colon>int)"
   4.165 +lemma int_Suc0_eq_1: "int (Suc 0) = 1"
   4.166  by simp
   4.167  
   4.168  text{*This version is proved for all ordered rings, not just integers!
   4.169 @@ -540,7 +543,7 @@
   4.170       "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
   4.171  by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
   4.172  
   4.173 -lemma negD: "(x \<Colon> int) < 0 \<Longrightarrow> \<exists>n. x = - (of_nat (Suc n))"
   4.174 +lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
   4.175  apply (cases x)
   4.176  apply (auto simp add: le minus Zero_int_def int_def order_less_le)
   4.177  apply (rule_tac x="y - Suc x" in exI, arith)
   4.178 @@ -553,7 +556,7 @@
   4.179  whether an integer is negative or not.*}
   4.180  
   4.181  theorem int_cases [case_names nonneg neg, cases type: int]:
   4.182 -  "[|!! n. (z \<Colon> int) = of_nat n ==> P;  !! n. z =  - (of_nat (Suc n)) ==> P |] ==> P"
   4.183 +  "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
   4.184  apply (cases "z < 0")
   4.185  apply (blast dest!: negD)
   4.186  apply (simp add: linorder_not_less del: of_nat_Suc)
   4.187 @@ -562,12 +565,12 @@
   4.188  done
   4.189  
   4.190  theorem int_of_nat_induct [case_names nonneg neg, induct type: int]:
   4.191 -     "[|!! n. P (of_nat n \<Colon> int);  !!n. P (- (of_nat (Suc n))) |] ==> P z"
   4.192 +     "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
   4.193    by (cases z) auto
   4.194  
   4.195  text{*Contributed by Brian Huffman*}
   4.196  theorem int_diff_cases:
   4.197 -  obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n"
   4.198 +  obtains (diff) m n where "z = int m - int n"
   4.199  apply (cases z rule: eq_Abs_Integ)
   4.200  apply (rule_tac m=x and n=y in diff)
   4.201  apply (simp add: int_def minus add diff_minus)
   4.202 @@ -944,11 +947,11 @@
   4.203    assumes number_of_eq: "number_of k = of_int k"
   4.204  
   4.205  class number_semiring = number + comm_semiring_1 +
   4.206 -  assumes number_of_int: "number_of (of_nat n) = of_nat n"
   4.207 +  assumes number_of_int: "number_of (int n) = of_nat n"
   4.208  
   4.209  instance number_ring \<subseteq> number_semiring
   4.210  proof
   4.211 -  fix n show "number_of (of_nat n) = (of_nat n :: 'a)"
   4.212 +  fix n show "number_of (int n) = (of_nat n :: 'a)"
   4.213      unfolding number_of_eq by (rule of_int_of_nat_eq)
   4.214  qed
   4.215  
   4.216 @@ -1124,7 +1127,7 @@
   4.217    show ?thesis
   4.218    proof
   4.219      assume eq: "1 + z + z = 0"
   4.220 -    have "(0::int) < 1 + (of_nat n + of_nat n)"
   4.221 +    have "(0::int) < 1 + (int n + int n)"
   4.222        by (simp add: le_imp_0_less add_increasing) 
   4.223      also have "... = - (1 + z + z)" 
   4.224        by (simp add: neg add_assoc [symmetric]) 
   4.225 @@ -1644,7 +1647,7 @@
   4.226  lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
   4.227  
   4.228  lemma split_nat [arith_split]:
   4.229 -  "P(nat(i::int)) = ((\<forall>n. i = of_nat n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
   4.230 +  "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
   4.231    (is "?P = (?L & ?R)")
   4.232  proof (cases "i < 0")
   4.233    case True thus ?thesis by auto
   4.234 @@ -1737,11 +1740,6 @@
   4.235      by (rule wf_subset [OF wf_measure]) 
   4.236  qed
   4.237  
   4.238 -abbreviation
   4.239 -  int :: "nat \<Rightarrow> int"
   4.240 -where
   4.241 -  "int \<equiv> of_nat"
   4.242 -
   4.243  (* `set:int': dummy construction *)
   4.244  theorem int_ge_induct [case_names base step, induct set: int]:
   4.245    fixes i :: int
     5.1 --- a/src/HOL/NSA/NSComplex.thy	Mon Sep 05 19:18:38 2011 +0200
     5.2 +++ b/src/HOL/NSA/NSComplex.thy	Tue Sep 06 07:23:45 2011 +0200
     5.3 @@ -613,7 +613,7 @@
     5.4  by (simp add: NSDeMoivre_ext)
     5.5  
     5.6  lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)"
     5.7 -by transfer (rule expi_add)
     5.8 +by transfer (rule exp_add)
     5.9  
    5.10  
    5.11  subsection{*@{term hcomplex_of_complex}: the Injection from
     6.1 --- a/src/HOL/Nominal/Nominal.thy	Mon Sep 05 19:18:38 2011 +0200
     6.2 +++ b/src/HOL/Nominal/Nominal.thy	Tue Sep 06 07:23:45 2011 +0200
     6.3 @@ -51,16 +51,16 @@
     6.4  begin
     6.5  
     6.6  definition
     6.7 -  perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) = (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
     6.8 +  "perm_fun pi f = (\<lambda>x. pi \<bullet> f (rev pi \<bullet> x))"
     6.9  
    6.10  definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
    6.11 -  perm_bool_def: "perm_bool pi b = b"
    6.12 +  "perm_bool pi b = b"
    6.13  
    6.14  primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit"  where 
    6.15    "perm_unit pi () = ()"
    6.16    
    6.17  primrec perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" where
    6.18 -  "perm_prod pi (x,y) = (pi\<bullet>x,pi\<bullet>y)"
    6.19 +  "perm_prod pi (x, y) = (pi\<bullet>x, pi\<bullet>y)"
    6.20  
    6.21  primrec perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    6.22    nil_eqvt:  "perm_list pi []     = []"
    6.23 @@ -71,13 +71,13 @@
    6.24  | none_eqvt:  "perm_option pi None     = None"
    6.25  
    6.26  definition perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char" where
    6.27 -  perm_char_def: "perm_char pi c = c"
    6.28 +  "perm_char pi c = c"
    6.29  
    6.30  definition perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat" where
    6.31 -  perm_nat_def: "perm_nat pi i = i"
    6.32 +  "perm_nat pi i = i"
    6.33  
    6.34  definition perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int" where
    6.35 -  perm_int_def: "perm_int pi i = i"
    6.36 +  "perm_int pi i = i"
    6.37  
    6.38  primrec perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" where
    6.39    nsome_eqvt:  "perm_noption pi (nSome x) = nSome (pi\<bullet>x)"
    6.40 @@ -962,7 +962,7 @@
    6.41    fixes pi::"'y prm"
    6.42    and   x ::"'x set"
    6.43    assumes dj: "disjoint TYPE('x) TYPE('y)"
    6.44 -  shows "(pi\<bullet>x)=x" 
    6.45 +  shows "pi\<bullet>x=x" 
    6.46    using dj by (simp_all add: perm_fun_def disjoint_def perm_bool)
    6.47  
    6.48  lemma dj_perm_perm_forget:
    6.49 @@ -1028,7 +1028,7 @@
    6.50  qed
    6.51  
    6.52  lemma pt_unit_inst:
    6.53 -  shows  "pt TYPE(unit) TYPE('x)"
    6.54 +  shows "pt TYPE(unit) TYPE('x)"
    6.55    by (simp add: pt_def)
    6.56  
    6.57  lemma pt_prod_inst:
     7.1 --- a/src/HOL/RComplete.thy	Mon Sep 05 19:18:38 2011 +0200
     7.2 +++ b/src/HOL/RComplete.thy	Tue Sep 06 07:23:45 2011 +0200
     7.3 @@ -475,12 +475,12 @@
     7.4    unfolding natceiling_def real_of_nat_def
     7.5    by (simp add: nat_le_iff ceiling_le_iff)
     7.6  
     7.7 -lemma natceiling_le_eq: "0 <= x ==> (natceiling x <= a) = (x <= real a)"
     7.8 -  unfolding natceiling_def real_of_nat_def (* FIXME: unused assumption *)
     7.9 +lemma natceiling_le_eq: "(natceiling x <= a) = (x <= real a)"
    7.10 +  unfolding natceiling_def real_of_nat_def
    7.11    by (simp add: nat_le_iff ceiling_le_iff)
    7.12  
    7.13  lemma natceiling_le_eq_number_of [simp]:
    7.14 -    "~ neg((number_of n)::int) ==> 0 <= x ==>
    7.15 +    "~ neg((number_of n)::int) ==>
    7.16        (natceiling x <= number_of n) = (x <= number_of n)"
    7.17    by (simp add: natceiling_le_eq)
    7.18  
     8.1 --- a/src/HOL/SEQ.thy	Mon Sep 05 19:18:38 2011 +0200
     8.2 +++ b/src/HOL/SEQ.thy	Tue Sep 06 07:23:45 2011 +0200
     8.3 @@ -380,22 +380,6 @@
     8.4    shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
     8.5  unfolding Bseq_conv_Bfun by (rule Bfun_inverse)
     8.6  
     8.7 -lemma LIMSEQ_add_const: (* FIXME: delete *)
     8.8 -  fixes a :: "'a::real_normed_vector"
     8.9 -  shows "f ----> a ==> (%n.(f n + b)) ----> a + b"
    8.10 -by (intro tendsto_intros)
    8.11 -
    8.12 -(* FIXME: delete *)
    8.13 -lemma LIMSEQ_add_minus:
    8.14 -  fixes a b :: "'a::real_normed_vector"
    8.15 -  shows "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
    8.16 -by (intro tendsto_intros)
    8.17 -
    8.18 -lemma LIMSEQ_diff_const: (* FIXME: delete *)
    8.19 -  fixes a b :: "'a::real_normed_vector"
    8.20 -  shows "f ----> a ==> (%n.(f n  - b)) ----> a - b"
    8.21 -by (intro tendsto_intros)
    8.22 -
    8.23  lemma LIMSEQ_diff_approach_zero:
    8.24    fixes L :: "'a::real_normed_vector"
    8.25    shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
    8.26 @@ -438,7 +422,8 @@
    8.27  
    8.28  lemma LIMSEQ_inverse_real_of_nat_add_minus:
    8.29       "(%n. r + -inverse(real(Suc n))) ----> r"
    8.30 -  using LIMSEQ_add_minus [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto
    8.31 +  using tendsto_add [OF tendsto_const
    8.32 +    tendsto_minus [OF LIMSEQ_inverse_real_of_nat]] by auto
    8.33  
    8.34  lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
    8.35       "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
    8.36 @@ -673,7 +658,6 @@
    8.37    "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
    8.38  by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
    8.39  
    8.40 -
    8.41  text{* Use completeness of reals (supremum property)
    8.42     to show that any bounded sequence has a least upper bound*}
    8.43  
    8.44 @@ -684,15 +668,8 @@
    8.45  
    8.46  subsubsection{*A Bounded and Monotonic Sequence Converges*}
    8.47  
    8.48 -lemma lemma_converg1:
    8.49 -     "!!(X::nat=>real). [| \<forall>m. \<forall> n \<ge> m. X m \<le> X n;
    8.50 -                  isLub (UNIV::real set) {x. \<exists>n. X n = x} (X ma)
    8.51 -               |] ==> \<forall>n \<ge> ma. X n = X ma"
    8.52 -apply safe
    8.53 -apply (drule_tac y = "X n" in isLubD2)
    8.54 -apply (blast dest: order_antisym)+
    8.55 -done
    8.56 -
    8.57 +(* TODO: delete *)
    8.58 +(* FIXME: one use in NSA/HSEQ.thy *)
    8.59  lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
    8.60  unfolding tendsto_def eventually_sequentially
    8.61  apply (rule_tac x = "X m" in exI, safe)
    8.62 @@ -700,50 +677,45 @@
    8.63  apply (drule spec, erule impE, auto)
    8.64  done
    8.65  
    8.66 -lemma lemma_converg2:
    8.67 -   "!!(X::nat=>real).
    8.68 -    [| \<forall>m. X m ~= U;  isLub UNIV {x. \<exists>n. X n = x} U |] ==> \<forall>m. X m < U"
    8.69 -apply safe
    8.70 -apply (drule_tac y = "X m" in isLubD2)
    8.71 -apply (auto dest!: order_le_imp_less_or_eq)
    8.72 -done
    8.73 -
    8.74 -lemma lemma_converg3: "!!(X ::nat=>real). \<forall>m. X m \<le> U ==> isUb UNIV {x. \<exists>n. X n = x} U"
    8.75 -by (rule setleI [THEN isUbI], auto)
    8.76 +text {* A monotone sequence converges to its least upper bound. *}
    8.77  
    8.78 -text{* FIXME: @{term "U - T < U"} is redundant *}
    8.79 -lemma lemma_converg4: "!!(X::nat=> real).
    8.80 -               [| \<forall>m. X m ~= U;
    8.81 -                  isLub UNIV {x. \<exists>n. X n = x} U;
    8.82 -                  0 < T;
    8.83 -                  U + - T < U
    8.84 -               |] ==> \<exists>m. U + -T < X m & X m < U"
    8.85 -apply (drule lemma_converg2, assumption)
    8.86 -apply (rule ccontr, simp)
    8.87 -apply (simp add: linorder_not_less)
    8.88 -apply (drule lemma_converg3)
    8.89 -apply (drule isLub_le_isUb, assumption)
    8.90 -apply (auto dest: order_less_le_trans)
    8.91 -done
    8.92 +lemma isLub_mono_imp_LIMSEQ:
    8.93 +  fixes X :: "nat \<Rightarrow> real"
    8.94 +  assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
    8.95 +  assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
    8.96 +  shows "X ----> u"
    8.97 +proof (rule LIMSEQ_I)
    8.98 +  have 1: "\<forall>n. X n \<le> u"
    8.99 +    using isLubD2 [OF u] by auto
   8.100 +  have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y"
   8.101 +    using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def)
   8.102 +  hence 2: "\<forall>y<u. \<exists>n. y < X n"
   8.103 +    by (metis not_le)
   8.104 +  fix r :: real assume "0 < r"
   8.105 +  hence "u - r < u" by simp
   8.106 +  hence "\<exists>m. u - r < X m" using 2 by simp
   8.107 +  then obtain m where "u - r < X m" ..
   8.108 +  with X have "\<forall>n\<ge>m. u - r < X n"
   8.109 +    by (fast intro: less_le_trans)
   8.110 +  hence "\<exists>m. \<forall>n\<ge>m. u - r < X n" ..
   8.111 +  thus "\<exists>m. \<forall>n\<ge>m. norm (X n - u) < r"
   8.112 +    using 1 by (simp add: diff_less_eq add_commute)
   8.113 +qed
   8.114  
   8.115  text{*A standard proof of the theorem for monotone increasing sequence*}
   8.116  
   8.117  lemma Bseq_mono_convergent:
   8.118       "[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent (X::nat=>real)"
   8.119 -apply (simp add: convergent_def)
   8.120 -apply (frule Bseq_isLub, safe)
   8.121 -apply (case_tac "\<exists>m. X m = U", auto)
   8.122 -apply (blast dest: lemma_converg1 Bmonoseq_LIMSEQ)
   8.123 -(* second case *)
   8.124 -apply (rule_tac x = U in exI)
   8.125 -apply (subst LIMSEQ_iff, safe)
   8.126 -apply (frule lemma_converg2, assumption)
   8.127 -apply (drule lemma_converg4, auto)
   8.128 -apply (rule_tac x = m in exI, safe)
   8.129 -apply (subgoal_tac "X m \<le> X n")
   8.130 - prefer 2 apply blast
   8.131 -apply (drule_tac x=n and P="%m. X m < U" in spec, arith)
   8.132 -done
   8.133 +proof -
   8.134 +  assume "Bseq X"
   8.135 +  then obtain u where u: "isLub UNIV {x. \<exists>n. X n = x} u"
   8.136 +    using Bseq_isLub by fast
   8.137 +  assume "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
   8.138 +  with u have "X ----> u"
   8.139 +    by (rule isLub_mono_imp_LIMSEQ)
   8.140 +  thus "convergent X"
   8.141 +    by (rule convergentI)
   8.142 +qed
   8.143  
   8.144  lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X"
   8.145  by (simp add: Bseq_def)
     9.1 --- a/src/HOL/Series.thy	Mon Sep 05 19:18:38 2011 +0200
     9.2 +++ b/src/HOL/Series.thy	Tue Sep 06 07:23:45 2011 +0200
     9.3 @@ -122,7 +122,7 @@
     9.4    shows "f sums s ==> (\<lambda>n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"
     9.5    apply (unfold sums_def)
     9.6    apply (simp add: sumr_offset)
     9.7 -  apply (rule LIMSEQ_diff_const)
     9.8 +  apply (rule tendsto_diff [OF _ tendsto_const])
     9.9    apply (rule LIMSEQ_ignore_initial_segment)
    9.10    apply assumption
    9.11  done
    9.12 @@ -166,7 +166,7 @@
    9.13  proof -
    9.14    from sumSuc[unfolded sums_def]
    9.15    have "(\<lambda>i. \<Sum>n = Suc 0..<Suc i. f n) ----> l" unfolding setsum_reindex[OF inj_Suc] image_Suc_atLeastLessThan[symmetric] comp_def .
    9.16 -  from LIMSEQ_add_const[OF this, where b="f 0"]
    9.17 +  from tendsto_add[OF this tendsto_const, where b="f 0"]
    9.18    have "(\<lambda>i. \<Sum>n = 0..<Suc i. f n) ----> l + f 0" unfolding add_commute setsum_head_upt_Suc[OF zero_less_Suc] .
    9.19    thus ?thesis unfolding sums_def by (rule LIMSEQ_imp_Suc)
    9.20  qed
    9.21 @@ -625,7 +625,7 @@
    9.22   apply (simp add:diff_Suc split:nat.splits)
    9.23   apply (blast intro: norm_ratiotest_lemma)
    9.24  apply (rule_tac x = "Suc N" in exI, clarify)
    9.25 -apply(simp cong:setsum_ivl_cong)
    9.26 +apply(simp cong del: setsum_cong cong: setsum_ivl_cong)
    9.27  done
    9.28  
    9.29  lemma ratio_test:
    10.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Sep 05 19:18:38 2011 +0200
    10.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Sep 06 07:23:45 2011 +0200
    10.3 @@ -475,8 +475,7 @@
    10.4      "op * = (%a b. nat (int a * int b))"
    10.5      "op div = (%a b. nat (int a div int b))"
    10.6      "op mod = (%a b. nat (int a mod int b))"
    10.7 -    by (auto intro!: ext simp add: nat_mult_distrib nat_div_distrib
    10.8 -      nat_mod_distrib)}
    10.9 +    by (fastsimp simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+}
   10.10  
   10.11    val ints = map mk_meta_eq @{lemma
   10.12      "int 0 = 0"
    11.1 --- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Sep 05 19:18:38 2011 +0200
    11.2 +++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Tue Sep 06 07:23:45 2011 +0200
    11.3 @@ -148,13 +148,11 @@
    11.4  end
    11.5  
    11.6  local
    11.7 -  fun equal_var cv (_, cu) = (cv aconvc cu)
    11.8 -
    11.9    fun prep (ct, vars) (maxidx, all_vars) =
   11.10      let
   11.11        val maxidx' = maxidx + maxidx_of ct + 1
   11.12  
   11.13 -      fun part (v as (i, cv)) =
   11.14 +      fun part (i, cv) =
   11.15          (case AList.lookup (op =) all_vars i of
   11.16            SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu))
   11.17          | NONE =>
    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Sep 05 19:18:38 2011 +0200
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Sep 06 07:23:45 2011 +0200
    12.3 @@ -124,18 +124,6 @@
    12.4      ss as _ :: _ => forall (is_prover_supported ctxt) ss
    12.5    | _ => false
    12.6  
    12.7 -(* "provers =" and "type_enc =" can be left out. The latter is a secret
    12.8 -   feature. *)
    12.9 -fun check_and_repair_raw_param ctxt (name, value) =
   12.10 -  if is_known_raw_param name then
   12.11 -    (name, value)
   12.12 -  else if is_prover_list ctxt name andalso null value then
   12.13 -    ("provers", [name])
   12.14 -  else if can (type_enc_from_string Sound) name andalso null value then
   12.15 -    ("type_enc", [name])
   12.16 -  else
   12.17 -    error ("Unknown parameter: " ^ quote name ^ ".")
   12.18 -
   12.19  fun unalias_raw_param (name, value) =
   12.20    case AList.lookup (op =) alias_params name of
   12.21      SOME name' => (name', value)
   12.22 @@ -148,6 +136,21 @@
   12.23                              | _ => value)
   12.24      | NONE => (name, value)
   12.25  
   12.26 +(* "provers =" and "type_enc =" can be left out. The latter is a secret
   12.27 +   feature. *)
   12.28 +fun normalize_raw_param ctxt =
   12.29 +  unalias_raw_param
   12.30 +  #> (fn (name, value) =>
   12.31 +         if is_known_raw_param name then
   12.32 +           (name, value)
   12.33 +         else if is_prover_list ctxt name andalso null value then
   12.34 +           ("provers", [name])
   12.35 +         else if can (type_enc_from_string Sound) name andalso null value then
   12.36 +           ("type_enc", [name])
   12.37 +         else
   12.38 +           error ("Unknown parameter: " ^ quote name ^ "."))
   12.39 +
   12.40 +
   12.41  (* Ensure that type systems such as "mono_simple!" and "mono_guards?" are
   12.42     handled correctly. *)
   12.43  fun implode_param [s, "?"] = s ^ "?"
   12.44 @@ -205,7 +208,10 @@
   12.45                                    max_default_remote_threads)
   12.46    |> implode_param
   12.47  
   12.48 -val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
   12.49 +fun set_default_raw_param param thy =
   12.50 +  let val ctxt = Proof_Context.init_global thy in
   12.51 +    thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param))
   12.52 +  end
   12.53  fun default_raw_params ctxt =
   12.54    let val thy = Proof_Context.theory_of ctxt in
   12.55      Data.get thy
   12.56 @@ -224,7 +230,6 @@
   12.57  
   12.58  fun extract_params mode default_params override_params =
   12.59    let
   12.60 -    val override_params = map unalias_raw_param override_params
   12.61      val raw_params = rev override_params @ rev default_params
   12.62      val lookup = Option.map implode_param o AList.lookup (op =) raw_params
   12.63      val lookup_string = the_default "" o lookup
   12.64 @@ -294,15 +299,15 @@
   12.65       timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   12.66    end
   12.67  
   12.68 -fun get_params mode ctxt = extract_params mode (default_raw_params ctxt)
   12.69 +fun get_params mode = extract_params mode o default_raw_params
   12.70  fun default_params thy = get_params Normal thy o map (apsnd single)
   12.71  
   12.72  (* Sledgehammer the given subgoal *)
   12.73  
   12.74  val default_minimize_prover = Metis_Tactic.metisN
   12.75  
   12.76 -val is_raw_param_relevant_for_minimize =
   12.77 -  member (op =) params_for_minimize o fst o unalias_raw_param
   12.78 +fun is_raw_param_relevant_for_minimize (name, _) =
   12.79 +  member (op =) params_for_minimize name
   12.80  fun string_for_raw_param (key, values) =
   12.81    key ^ (case implode_param values of "" => "" | value => " = " ^ value)
   12.82  
   12.83 @@ -324,8 +329,7 @@
   12.84  fun hammer_away override_params subcommand opt_i relevance_override state =
   12.85    let
   12.86      val ctxt = Proof.context_of state
   12.87 -    val override_params =
   12.88 -      override_params |> map (check_and_repair_raw_param ctxt)
   12.89 +    val override_params = override_params |> map (normalize_raw_param ctxt)
   12.90    in
   12.91      if subcommand = runN then
   12.92        let val i = the_default 1 opt_i in
   12.93 @@ -368,8 +372,7 @@
   12.94                               (case default_raw_params ctxt |> rev of
   12.95                                  [] => "none"
   12.96                                | params =>
   12.97 -                                params |> map (check_and_repair_raw_param ctxt)
   12.98 -                                       |> map string_for_raw_param
   12.99 +                                params |> map string_for_raw_param
  12.100                                         |> sort_strings |> cat_lines))
  12.101                    end))
  12.102  
    13.1 --- a/src/HOL/Tools/monomorph.ML	Mon Sep 05 19:18:38 2011 +0200
    13.2 +++ b/src/HOL/Tools/monomorph.ML	Tue Sep 06 07:23:45 2011 +0200
    13.3 @@ -319,7 +319,7 @@
    13.4      val (thm_infos, (known_grounds, subs)) = prepare schematic_consts_of rthms
    13.5    in
    13.6      if Symtab.is_empty known_grounds then
    13.7 -      (map (single o pair 0 o snd) rthms, ctxt)
    13.8 +      (map (fn Ground thm => [(0, thm)] | _ => []) thm_infos, ctxt)
    13.9      else
   13.10        make_subst_ctxt ctxt thm_infos known_grounds subs
   13.11        |> limit_rounds ctxt (collect_substitutions thm_infos)
    14.1 --- a/src/HOL/Transcendental.thy	Mon Sep 05 19:18:38 2011 +0200
    14.2 +++ b/src/HOL/Transcendental.thy	Tue Sep 06 07:23:45 2011 +0200
    14.3 @@ -1999,7 +1999,7 @@
    14.4  apply (drule tan_total_pos)
    14.5  apply (cut_tac [2] y="-y" in tan_total_pos, safe)
    14.6  apply (rule_tac [3] x = "-x" in exI)
    14.7 -apply (auto intro!: exI)
    14.8 +apply (auto del: exI intro!: exI)
    14.9  done
   14.10  
   14.11  lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
   14.12 @@ -2009,7 +2009,7 @@
   14.13  apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
   14.14  apply (rule_tac [4] Rolle)
   14.15  apply (rule_tac [2] Rolle)
   14.16 -apply (auto intro!: DERIV_tan DERIV_isCont exI
   14.17 +apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI
   14.18              simp add: differentiable_def)
   14.19  txt{*Now, simulate TRYALL*}
   14.20  apply (rule_tac [!] DERIV_tan asm_rl)
   14.21 @@ -2785,7 +2785,7 @@
   14.22          have "norm (?diff 1 n - 0) < r" by auto }
   14.23        thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
   14.24      qed
   14.25 -    from this[unfolded tendsto_rabs_zero_iff diff_minus add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN tendsto_minus]
   14.26 +    from this [unfolded tendsto_rabs_zero_iff, THEN tendsto_add [OF _ tendsto_const], of "- arctan 1", THEN tendsto_minus]
   14.27      have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
   14.28      hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
   14.29  
    15.1 --- a/src/HOL/Unix/Nested_Environment.thy	Mon Sep 05 19:18:38 2011 +0200
    15.2 +++ b/src/HOL/Unix/Nested_Environment.thy	Tue Sep 06 07:23:45 2011 +0200
    15.3 @@ -9,7 +9,7 @@
    15.4  begin
    15.5  
    15.6  text {*
    15.7 -  Consider a partial function @{term [source] "e :: 'a => 'b option"};
    15.8 +  Consider a partial function @{term [source] "e :: 'a \<Rightarrow> 'b option"};
    15.9    this may be understood as an \emph{environment} mapping indexes
   15.10    @{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory
   15.11    @{text Map} of Isabelle/HOL).  This basic idea is easily generalized
   15.12 @@ -21,7 +21,7 @@
   15.13  
   15.14  datatype ('a, 'b, 'c) env =
   15.15      Val 'a
   15.16 -  | Env 'b  "'c => ('a, 'b, 'c) env option"
   15.17 +  | Env 'b  "'c \<Rightarrow> ('a, 'b, 'c) env option"
   15.18  
   15.19  text {*
   15.20    \medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ
   15.21 @@ -43,14 +43,14 @@
   15.22    @{term None}.
   15.23  *}
   15.24  
   15.25 -primrec lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
   15.26 -  and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option"
   15.27 +primrec lookup :: "('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"
   15.28 +  and lookup_option :: "('a, 'b, 'c) env option \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"
   15.29  where
   15.30      "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
   15.31    | "lookup (Env b es) xs =
   15.32        (case xs of
   15.33 -        [] => Some (Env b es)
   15.34 -      | y # ys => lookup_option (es y) ys)"
   15.35 +        [] \<Rightarrow> Some (Env b es)
   15.36 +      | y # ys \<Rightarrow> lookup_option (es y) ys)"
   15.37    | "lookup_option None xs = None"
   15.38    | "lookup_option (Some e) xs = lookup e xs"
   15.39  
   15.40 @@ -70,8 +70,8 @@
   15.41  theorem lookup_env_cons:
   15.42    "lookup (Env b es) (x # xs) =
   15.43      (case es x of
   15.44 -      None => None
   15.45 -    | Some e => lookup e xs)"
   15.46 +      None \<Rightarrow> None
   15.47 +    | Some e \<Rightarrow> lookup e xs)"
   15.48    by (cases "es x") simp_all
   15.49  
   15.50  lemmas lookup_lookup_option.simps [simp del]
   15.51 @@ -80,14 +80,14 @@
   15.52  theorem lookup_eq:
   15.53    "lookup env xs =
   15.54      (case xs of
   15.55 -      [] => Some env
   15.56 -    | x # xs =>
   15.57 +      [] \<Rightarrow> Some env
   15.58 +    | x # xs \<Rightarrow>
   15.59        (case env of
   15.60 -        Val a => None
   15.61 -      | Env b es =>
   15.62 +        Val a \<Rightarrow> None
   15.63 +      | Env b es \<Rightarrow>
   15.64            (case es x of
   15.65 -            None => None
   15.66 -          | Some e => lookup e xs)))"
   15.67 +            None \<Rightarrow> None
   15.68 +          | Some e \<Rightarrow> lookup e xs)))"
   15.69    by (simp split: list.split env.split)
   15.70  
   15.71  text {*
   15.72 @@ -245,18 +245,18 @@
   15.73    environment is left unchanged.
   15.74  *}
   15.75  
   15.76 -primrec update :: "'c list => ('a, 'b, 'c) env option =>
   15.77 -    ('a, 'b, 'c) env => ('a, 'b, 'c) env"
   15.78 -  and update_option :: "'c list => ('a, 'b, 'c) env option =>
   15.79 -    ('a, 'b, 'c) env option => ('a, 'b, 'c) env option"
   15.80 +primrec update :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>
   15.81 +    ('a, 'b, 'c) env \<Rightarrow> ('a, 'b, 'c) env"
   15.82 +  and update_option :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>
   15.83 +    ('a, 'b, 'c) env option \<Rightarrow> ('a, 'b, 'c) env option"
   15.84  where
   15.85    "update xs opt (Val a) =
   15.86 -    (if xs = [] then (case opt of None => Val a | Some e => e)
   15.87 +    (if xs = [] then (case opt of None \<Rightarrow> Val a | Some e \<Rightarrow> e)
   15.88       else Val a)"
   15.89  | "update xs opt (Env b es) =
   15.90      (case xs of
   15.91 -      [] => (case opt of None => Env b es | Some e => e)
   15.92 -    | y # ys => Env b (es (y := update_option ys opt (es y))))"
   15.93 +      [] \<Rightarrow> (case opt of None \<Rightarrow> Env b es | Some e \<Rightarrow> e)
   15.94 +    | y # ys \<Rightarrow> Env b (es (y := update_option ys opt (es y))))"
   15.95  | "update_option xs opt None =
   15.96      (if xs = [] then opt else None)"
   15.97  | "update_option xs opt (Some e) =
   15.98 @@ -286,8 +286,8 @@
   15.99    "update (x # y # ys) opt (Env b es) =
  15.100      Env b (es (x :=
  15.101        (case es x of
  15.102 -        None => None
  15.103 -      | Some e => Some (update (y # ys) opt e))))"
  15.104 +        None \<Rightarrow> None
  15.105 +      | Some e \<Rightarrow> Some (update (y # ys) opt e))))"
  15.106    by (cases "es x") simp_all
  15.107  
  15.108  lemmas update_update_option.simps [simp del]
  15.109 @@ -297,21 +297,21 @@
  15.110  lemma update_eq:
  15.111    "update xs opt env =
  15.112      (case xs of
  15.113 -      [] =>
  15.114 +      [] \<Rightarrow>
  15.115          (case opt of
  15.116 -          None => env
  15.117 -        | Some e => e)
  15.118 -    | x # xs =>
  15.119 +          None \<Rightarrow> env
  15.120 +        | Some e \<Rightarrow> e)
  15.121 +    | x # xs \<Rightarrow>
  15.122          (case env of
  15.123 -          Val a => Val a
  15.124 -        | Env b es =>
  15.125 +          Val a \<Rightarrow> Val a
  15.126 +        | Env b es \<Rightarrow>
  15.127              (case xs of
  15.128 -              [] => Env b (es (x := opt))
  15.129 -            | y # ys =>
  15.130 +              [] \<Rightarrow> Env b (es (x := opt))
  15.131 +            | y # ys \<Rightarrow>
  15.132                  Env b (es (x :=
  15.133                    (case es x of
  15.134 -                    None => None
  15.135 -                  | Some e => Some (update (y # ys) opt e)))))))"
  15.136 +                    None \<Rightarrow> None
  15.137 +                  | Some e \<Rightarrow> Some (update (y # ys) opt e)))))))"
  15.138    by (simp split: list.split env.split option.split)
  15.139  
  15.140  text {*
    16.1 --- a/src/Pure/General/markup.ML	Mon Sep 05 19:18:38 2011 +0200
    16.2 +++ b/src/Pure/General/markup.ML	Tue Sep 06 07:23:45 2011 +0200
    16.3 @@ -58,7 +58,6 @@
    16.4    val propN: string val prop: T
    16.5    val ML_keywordN: string val ML_keyword: T
    16.6    val ML_delimiterN: string val ML_delimiter: T
    16.7 -  val ML_identN: string val ML_ident: T
    16.8    val ML_tvarN: string val ML_tvar: T
    16.9    val ML_numeralN: string val ML_numeral: T
   16.10    val ML_charN: string val ML_char: T
   16.11 @@ -80,7 +79,6 @@
   16.12    val keywordN: string val keyword: T
   16.13    val operatorN: string val operator: T
   16.14    val commandN: string val command: T
   16.15 -  val identN: string val ident: T
   16.16    val stringN: string val string: T
   16.17    val altstringN: string val altstring: T
   16.18    val verbatimN: string val verbatim: T
   16.19 @@ -257,7 +255,6 @@
   16.20  
   16.21  val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
   16.22  val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
   16.23 -val (ML_identN, ML_ident) = markup_elem "ML_ident";
   16.24  val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
   16.25  val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
   16.26  val (ML_charN, ML_char) = markup_elem "ML_char";
   16.27 @@ -292,7 +289,6 @@
   16.28  val (keywordN, keyword) = markup_elem "keyword";
   16.29  val (operatorN, operator) = markup_elem "operator";
   16.30  val (commandN, command) = markup_elem "command";
   16.31 -val (identN, ident) = markup_elem "ident";
   16.32  val (stringN, string) = markup_elem "string";
   16.33  val (altstringN, altstring) = markup_elem "altstring";
   16.34  val (verbatimN, verbatim) = markup_elem "verbatim";
    17.1 --- a/src/Pure/General/markup.scala	Mon Sep 05 19:18:38 2011 +0200
    17.2 +++ b/src/Pure/General/markup.scala	Tue Sep 06 07:23:45 2011 +0200
    17.3 @@ -142,7 +142,6 @@
    17.4  
    17.5    val ML_KEYWORD = "ML_keyword"
    17.6    val ML_DELIMITER = "ML_delimiter"
    17.7 -  val ML_IDENT = "ML_ident"
    17.8    val ML_TVAR = "ML_tvar"
    17.9    val ML_NUMERAL = "ML_numeral"
   17.10    val ML_CHAR = "ML_char"
   17.11 @@ -164,7 +163,6 @@
   17.12    val KEYWORD = "keyword"
   17.13    val OPERATOR = "operator"
   17.14    val COMMAND = "command"
   17.15 -  val IDENT = "ident"
   17.16    val STRING = "string"
   17.17    val ALTSTRING = "altstring"
   17.18    val VERBATIM = "verbatim"
    18.1 --- a/src/Pure/General/timing.scala	Mon Sep 05 19:18:38 2011 +0200
    18.2 +++ b/src/Pure/General/timing.scala	Tue Sep 06 07:23:45 2011 +0200
    18.3 @@ -9,6 +9,7 @@
    18.4  object Time
    18.5  {
    18.6    def seconds(s: Double): Time = new Time((s * 1000.0) round)
    18.7 +  def ms(m: Long): Time = new Time(m)
    18.8  }
    18.9  
   18.10  class Time(val ms: Long)
    19.1 --- a/src/Pure/General/xml.ML	Mon Sep 05 19:18:38 2011 +0200
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,361 +0,0 @@
    19.4 -(*  Title:      Pure/General/xml.ML
    19.5 -    Author:     David Aspinall, Stefan Berghofer and Markus Wenzel
    19.6 -
    19.7 -Untyped XML trees.
    19.8 -*)
    19.9 -
   19.10 -signature XML_DATA_OPS =
   19.11 -sig
   19.12 -  type 'a A
   19.13 -  type 'a T
   19.14 -  type 'a V
   19.15 -  val int_atom: int A
   19.16 -  val bool_atom: bool A
   19.17 -  val unit_atom: unit A
   19.18 -  val properties: Properties.T T
   19.19 -  val string: string T
   19.20 -  val int: int T
   19.21 -  val bool: bool T
   19.22 -  val unit: unit T
   19.23 -  val pair: 'a T -> 'b T -> ('a * 'b) T
   19.24 -  val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
   19.25 -  val list: 'a T -> 'a list T
   19.26 -  val option: 'a T -> 'a option T
   19.27 -  val variant: 'a V list -> 'a T
   19.28 -end;
   19.29 -
   19.30 -signature XML =
   19.31 -sig
   19.32 -  type attributes = Properties.T
   19.33 -  datatype tree =
   19.34 -      Elem of Markup.T * tree list
   19.35 -    | Text of string
   19.36 -  type body = tree list
   19.37 -  val add_content: tree -> Buffer.T -> Buffer.T
   19.38 -  val content_of: body -> string
   19.39 -  val header: string
   19.40 -  val text: string -> string
   19.41 -  val element: string -> attributes -> string list -> string
   19.42 -  val output_markup: Markup.T -> Output.output * Output.output
   19.43 -  val string_of: tree -> string
   19.44 -  val pretty: int -> tree -> Pretty.T
   19.45 -  val output: tree -> TextIO.outstream -> unit
   19.46 -  val parse_comments: string list -> unit * string list
   19.47 -  val parse_string : string -> string option
   19.48 -  val parse_element: string list -> tree * string list
   19.49 -  val parse_document: string list -> tree * string list
   19.50 -  val parse: string -> tree
   19.51 -  exception XML_ATOM of string
   19.52 -  exception XML_BODY of body
   19.53 -  structure Encode: XML_DATA_OPS
   19.54 -  structure Decode: XML_DATA_OPS
   19.55 -end;
   19.56 -
   19.57 -structure XML: XML =
   19.58 -struct
   19.59 -
   19.60 -(** XML trees **)
   19.61 -
   19.62 -type attributes = Properties.T;
   19.63 -
   19.64 -datatype tree =
   19.65 -    Elem of Markup.T * tree list
   19.66 -  | Text of string;
   19.67 -
   19.68 -type body = tree list;
   19.69 -
   19.70 -fun add_content (Elem (_, ts)) = fold add_content ts
   19.71 -  | add_content (Text s) = Buffer.add s;
   19.72 -
   19.73 -fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
   19.74 -
   19.75 -
   19.76 -
   19.77 -(** string representation **)
   19.78 -
   19.79 -val header = "<?xml version=\"1.0\"?>\n";
   19.80 -
   19.81 -
   19.82 -(* escaped text *)
   19.83 -
   19.84 -fun decode "&lt;" = "<"
   19.85 -  | decode "&gt;" = ">"
   19.86 -  | decode "&amp;" = "&"
   19.87 -  | decode "&apos;" = "'"
   19.88 -  | decode "&quot;" = "\""
   19.89 -  | decode c = c;
   19.90 -
   19.91 -fun encode "<" = "&lt;"
   19.92 -  | encode ">" = "&gt;"
   19.93 -  | encode "&" = "&amp;"
   19.94 -  | encode "'" = "&apos;"
   19.95 -  | encode "\"" = "&quot;"
   19.96 -  | encode c = c;
   19.97 -
   19.98 -val text = translate_string encode;
   19.99 -
  19.100 -
  19.101 -(* elements *)
  19.102 -
  19.103 -fun elem name atts =
  19.104 -  space_implode " " (name :: map (fn (a, x) => a ^ "=\"" ^ text x ^ "\"") atts);
  19.105 -
  19.106 -fun element name atts body =
  19.107 -  let val b = implode body in
  19.108 -    if b = "" then enclose "<" "/>" (elem name atts)
  19.109 -    else enclose "<" ">" (elem name atts) ^ b ^ enclose "</" ">" name
  19.110 -  end;
  19.111 -
  19.112 -fun output_markup (markup as (name, atts)) =
  19.113 -  if Markup.is_empty markup then Markup.no_output
  19.114 -  else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
  19.115 -
  19.116 -
  19.117 -(* output *)
  19.118 -
  19.119 -fun buffer_of depth tree =
  19.120 -  let
  19.121 -    fun traverse _ (Elem ((name, atts), [])) =
  19.122 -          Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
  19.123 -      | traverse d (Elem ((name, atts), ts)) =
  19.124 -          Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
  19.125 -          traverse_body d ts #>
  19.126 -          Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
  19.127 -      | traverse _ (Text s) = Buffer.add (text s)
  19.128 -    and traverse_body 0 _ = Buffer.add "..."
  19.129 -      | traverse_body d ts = fold (traverse (d - 1)) ts;
  19.130 -  in Buffer.empty |> traverse depth tree end;
  19.131 -
  19.132 -val string_of = Buffer.content o buffer_of ~1;
  19.133 -val output = Buffer.output o buffer_of ~1;
  19.134 -
  19.135 -fun pretty depth tree =
  19.136 -  Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
  19.137 -
  19.138 -
  19.139 -
  19.140 -(** XML parsing (slow) **)
  19.141 -
  19.142 -local
  19.143 -
  19.144 -fun err msg (xs, _) =
  19.145 -  fn () => "XML parsing error: " ^ msg () ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
  19.146 -
  19.147 -fun ignored _ = [];
  19.148 -
  19.149 -val blanks = Scan.many Symbol.is_blank;
  19.150 -val special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
  19.151 -val regular = Scan.one Symbol.is_regular;
  19.152 -fun regular_except x = Scan.one (fn c => Symbol.is_regular c andalso c <> x);
  19.153 -
  19.154 -val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode;
  19.155 -
  19.156 -val parse_cdata =
  19.157 -  Scan.this_string "<![CDATA[" |--
  19.158 -  (Scan.repeat (Scan.unless (Scan.this_string "]]>") regular) >> implode) --|
  19.159 -  Scan.this_string "]]>";
  19.160 -
  19.161 -val parse_att =
  19.162 -  (Symbol.scan_id --| (blanks -- $$ "=" -- blanks)) --
  19.163 -  (($$ "\"" || $$ "'") :|-- (fn s =>
  19.164 -    (Scan.repeat (special || regular_except s) >> implode) --| $$ s));
  19.165 -
  19.166 -val parse_comment =
  19.167 -  Scan.this_string "<!--" --
  19.168 -  Scan.repeat (Scan.unless (Scan.this_string "-->") regular) --
  19.169 -  Scan.this_string "-->" >> ignored;
  19.170 -
  19.171 -val parse_processing_instruction =
  19.172 -  Scan.this_string "<?" --
  19.173 -  Scan.repeat (Scan.unless (Scan.this_string "?>") regular) --
  19.174 -  Scan.this_string "?>" >> ignored;
  19.175 -
  19.176 -val parse_doctype =
  19.177 -  Scan.this_string "<!DOCTYPE" --
  19.178 -  Scan.repeat (Scan.unless ($$ ">") regular) --
  19.179 -  $$ ">" >> ignored;
  19.180 -
  19.181 -val parse_misc =
  19.182 -  Scan.one Symbol.is_blank >> ignored ||
  19.183 -  parse_processing_instruction ||
  19.184 -  parse_comment;
  19.185 -
  19.186 -val parse_optional_text =
  19.187 -  Scan.optional (parse_chars >> (single o Text)) [];
  19.188 -
  19.189 -fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_";
  19.190 -fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = ".";
  19.191 -val parse_name = Scan.one name_start_char ::: Scan.many name_char;
  19.192 -
  19.193 -in
  19.194 -
  19.195 -val parse_comments =
  19.196 -  blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K ();
  19.197 -
  19.198 -val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode;
  19.199 -
  19.200 -fun parse_content xs =
  19.201 -  (parse_optional_text @@@
  19.202 -    (Scan.repeat
  19.203 -      ((parse_element >> single ||
  19.204 -        parse_cdata >> (single o Text) ||
  19.205 -        parse_processing_instruction ||
  19.206 -        parse_comment)
  19.207 -      @@@ parse_optional_text) >> flat)) xs
  19.208 -
  19.209 -and parse_element xs =
  19.210 -  ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--
  19.211 -    (fn (name, _) =>
  19.212 -      !! (err (fn () => "Expected > or />"))
  19.213 -       ($$ "/" -- $$ ">" >> ignored ||
  19.214 -        $$ ">" |-- parse_content --|
  19.215 -          !! (err (fn () => "Expected </" ^ implode name ^ ">"))
  19.216 -              ($$ "<" -- $$ "/" -- Scan.this name -- blanks -- $$ ">")))
  19.217 -    >> (fn ((name, atts), body) => Elem ((implode name, atts), body))) xs;
  19.218 -
  19.219 -val parse_document =
  19.220 -  (Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc)
  19.221 -  |-- parse_element;
  19.222 -
  19.223 -fun parse s =
  19.224 -  (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element"))
  19.225 -      (blanks |-- parse_document --| blanks))) (raw_explode s) of
  19.226 -    (x, []) => x
  19.227 -  | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));
  19.228 -
  19.229 -end;
  19.230 -
  19.231 -
  19.232 -
  19.233 -(** XML as data representation language **)
  19.234 -
  19.235 -exception XML_ATOM of string;
  19.236 -exception XML_BODY of tree list;
  19.237 -
  19.238 -
  19.239 -structure Encode =
  19.240 -struct
  19.241 -
  19.242 -type 'a A = 'a -> string;
  19.243 -type 'a T = 'a -> body;
  19.244 -type 'a V = 'a -> string list * body;
  19.245 -
  19.246 -
  19.247 -(* atomic values *)
  19.248 -
  19.249 -fun int_atom i = signed_string_of_int i;
  19.250 -
  19.251 -fun bool_atom false = "0"
  19.252 -  | bool_atom true = "1";
  19.253 -
  19.254 -fun unit_atom () = "";
  19.255 -
  19.256 -
  19.257 -(* structural nodes *)
  19.258 -
  19.259 -fun node ts = Elem ((":", []), ts);
  19.260 -
  19.261 -fun vector xs = map_index (fn (i, x) => (int_atom i, x)) xs;
  19.262 -
  19.263 -fun tagged (tag, (xs, ts)) = Elem ((int_atom tag, vector xs), ts);
  19.264 -
  19.265 -
  19.266 -(* representation of standard types *)
  19.267 -
  19.268 -fun properties props = [Elem ((":", props), [])];
  19.269 -
  19.270 -fun string "" = []
  19.271 -  | string s = [Text s];
  19.272 -
  19.273 -val int = string o int_atom;
  19.274 -
  19.275 -val bool = string o bool_atom;
  19.276 -
  19.277 -val unit = string o unit_atom;
  19.278 -
  19.279 -fun pair f g (x, y) = [node (f x), node (g y)];
  19.280 -
  19.281 -fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
  19.282 -
  19.283 -fun list f xs = map (node o f) xs;
  19.284 -
  19.285 -fun option _ NONE = []
  19.286 -  | option f (SOME x) = [node (f x)];
  19.287 -
  19.288 -fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
  19.289 -
  19.290 -end;
  19.291 -
  19.292 -
  19.293 -structure Decode =
  19.294 -struct
  19.295 -
  19.296 -type 'a A = string -> 'a;
  19.297 -type 'a T = body -> 'a;
  19.298 -type 'a V = string list * body -> 'a;
  19.299 -
  19.300 -
  19.301 -(* atomic values *)
  19.302 -
  19.303 -fun int_atom s =
  19.304 -  Markup.parse_int s
  19.305 -    handle Fail _ => raise XML_ATOM s;
  19.306 -
  19.307 -fun bool_atom "0" = false
  19.308 -  | bool_atom "1" = true
  19.309 -  | bool_atom s = raise XML_ATOM s;
  19.310 -
  19.311 -fun unit_atom "" = ()
  19.312 -  | unit_atom s = raise XML_ATOM s;
  19.313 -
  19.314 -
  19.315 -(* structural nodes *)
  19.316 -
  19.317 -fun node (Elem ((":", []), ts)) = ts
  19.318 -  | node t = raise XML_BODY [t];
  19.319 -
  19.320 -fun vector atts =
  19.321 -  #1 (fold_map (fn (a, x) =>
  19.322 -        fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts 0);
  19.323 -
  19.324 -fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
  19.325 -  | tagged t = raise XML_BODY [t];
  19.326 -
  19.327 -
  19.328 -(* representation of standard types *)
  19.329 -
  19.330 -fun properties [Elem ((":", props), [])] = props
  19.331 -  | properties ts = raise XML_BODY ts;
  19.332 -
  19.333 -fun string [] = ""
  19.334 -  | string [Text s] = s
  19.335 -  | string ts = raise XML_BODY ts;
  19.336 -
  19.337 -val int = int_atom o string;
  19.338 -
  19.339 -val bool = bool_atom o string;
  19.340 -
  19.341 -val unit = unit_atom o string;
  19.342 -
  19.343 -fun pair f g [t1, t2] = (f (node t1), g (node t2))
  19.344 -  | pair _ _ ts = raise XML_BODY ts;
  19.345 -
  19.346 -fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
  19.347 -  | triple _ _ _ ts = raise XML_BODY ts;
  19.348 -
  19.349 -fun list f ts = map (f o node) ts;
  19.350 -
  19.351 -fun option _ [] = NONE
  19.352 -  | option f [t] = SOME (f (node t))
  19.353 -  | option _ ts = raise XML_BODY ts;
  19.354 -
  19.355 -fun variant fs [t] =
  19.356 -      let
  19.357 -        val (tag, (xs, ts)) = tagged t;
  19.358 -        val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
  19.359 -      in f (xs, ts) end
  19.360 -  | variant _ ts = raise XML_BODY ts;
  19.361 -
  19.362 -end;
  19.363 -
  19.364 -end;
    20.1 --- a/src/Pure/General/xml.scala	Mon Sep 05 19:18:38 2011 +0200
    20.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.3 @@ -1,390 +0,0 @@
    20.4 -/*  Title:      Pure/General/xml.scala
    20.5 -    Author:     Makarius
    20.6 -
    20.7 -Untyped XML trees.
    20.8 -*/
    20.9 -
   20.10 -package isabelle
   20.11 -
   20.12 -import java.lang.System
   20.13 -import java.util.WeakHashMap
   20.14 -import java.lang.ref.WeakReference
   20.15 -import javax.xml.parsers.DocumentBuilderFactory
   20.16 -
   20.17 -import scala.actors.Actor._
   20.18 -import scala.collection.mutable
   20.19 -
   20.20 -
   20.21 -object XML
   20.22 -{
   20.23 -  /** XML trees **/
   20.24 -
   20.25 -  /* datatype representation */
   20.26 -
   20.27 -  type Attributes = Properties.T
   20.28 -
   20.29 -  sealed abstract class Tree { override def toString = string_of_tree(this) }
   20.30 -  case class Elem(markup: Markup, body: List[Tree]) extends Tree
   20.31 -  case class Text(content: String) extends Tree
   20.32 -
   20.33 -  def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
   20.34 -  def elem(name: String) = Elem(Markup(name, Nil), Nil)
   20.35 -
   20.36 -  type Body = List[Tree]
   20.37 -
   20.38 -
   20.39 -  /* string representation */
   20.40 -
   20.41 -  def string_of_body(body: Body): String =
   20.42 -  {
   20.43 -    val s = new StringBuilder
   20.44 -
   20.45 -    def text(txt: String) {
   20.46 -      if (txt == null) s ++= txt
   20.47 -      else {
   20.48 -        for (c <- txt.iterator) c match {
   20.49 -          case '<' => s ++= "&lt;"
   20.50 -          case '>' => s ++= "&gt;"
   20.51 -          case '&' => s ++= "&amp;"
   20.52 -          case '"' => s ++= "&quot;"
   20.53 -          case '\'' => s ++= "&apos;"
   20.54 -          case _ => s += c
   20.55 -        }
   20.56 -      }
   20.57 -    }
   20.58 -    def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
   20.59 -    def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
   20.60 -    def tree(t: Tree): Unit =
   20.61 -      t match {
   20.62 -        case Elem(markup, Nil) =>
   20.63 -          s ++= "<"; elem(markup); s ++= "/>"
   20.64 -        case Elem(markup, ts) =>
   20.65 -          s ++= "<"; elem(markup); s ++= ">"
   20.66 -          ts.foreach(tree)
   20.67 -          s ++= "</"; s ++= markup.name; s ++= ">"
   20.68 -        case Text(txt) => text(txt)
   20.69 -      }
   20.70 -    body.foreach(tree)
   20.71 -    s.toString
   20.72 -  }
   20.73 -
   20.74 -  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
   20.75 -
   20.76 -
   20.77 -  /* text content */
   20.78 -
   20.79 -  def content_stream(tree: Tree): Stream[String] =
   20.80 -    tree match {
   20.81 -      case Elem(_, body) => content_stream(body)
   20.82 -      case Text(content) => Stream(content)
   20.83 -    }
   20.84 -  def content_stream(body: Body): Stream[String] =
   20.85 -    body.toStream.flatten(content_stream(_))
   20.86 -
   20.87 -  def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
   20.88 -  def content(body: Body): Iterator[String] = content_stream(body).iterator
   20.89 -
   20.90 -
   20.91 -  /* pipe-lined cache for partial sharing */
   20.92 -
   20.93 -  class Cache(initial_size: Int = 131071, max_string: Int = 100)
   20.94 -  {
   20.95 -    private val cache_actor = actor
   20.96 -    {
   20.97 -      val table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
   20.98 -
   20.99 -      def lookup[A](x: A): Option[A] =
  20.100 -      {
  20.101 -        val ref = table.get(x)
  20.102 -        if (ref == null) None
  20.103 -        else {
  20.104 -          val y = ref.asInstanceOf[WeakReference[A]].get
  20.105 -          if (y == null) None
  20.106 -          else Some(y)
  20.107 -        }
  20.108 -      }
  20.109 -      def store[A](x: A): A =
  20.110 -      {
  20.111 -        table.put(x, new WeakReference[Any](x))
  20.112 -        x
  20.113 -      }
  20.114 -
  20.115 -      def trim_bytes(s: String): String = new String(s.toCharArray)
  20.116 -
  20.117 -      def cache_string(x: String): String =
  20.118 -        lookup(x) match {
  20.119 -          case Some(y) => y
  20.120 -          case None =>
  20.121 -            val z = trim_bytes(x)
  20.122 -            if (z.length > max_string) z else store(z)
  20.123 -        }
  20.124 -      def cache_props(x: Properties.T): Properties.T =
  20.125 -        if (x.isEmpty) x
  20.126 -        else
  20.127 -          lookup(x) match {
  20.128 -            case Some(y) => y
  20.129 -            case None => store(x.map(p => (trim_bytes(p._1).intern, cache_string(p._2))))
  20.130 -          }
  20.131 -      def cache_markup(x: Markup): Markup =
  20.132 -        lookup(x) match {
  20.133 -          case Some(y) => y
  20.134 -          case None =>
  20.135 -            x match {
  20.136 -              case Markup(name, props) =>
  20.137 -                store(Markup(cache_string(name), cache_props(props)))
  20.138 -            }
  20.139 -        }
  20.140 -      def cache_tree(x: XML.Tree): XML.Tree =
  20.141 -        lookup(x) match {
  20.142 -          case Some(y) => y
  20.143 -          case None =>
  20.144 -            x match {
  20.145 -              case XML.Elem(markup, body) =>
  20.146 -                store(XML.Elem(cache_markup(markup), cache_body(body)))
  20.147 -              case XML.Text(text) => store(XML.Text(cache_string(text)))
  20.148 -            }
  20.149 -        }
  20.150 -      def cache_body(x: XML.Body): XML.Body =
  20.151 -        if (x.isEmpty) x
  20.152 -        else
  20.153 -          lookup(x) match {
  20.154 -            case Some(y) => y
  20.155 -            case None => x.map(cache_tree(_))
  20.156 -          }
  20.157 -
  20.158 -      // main loop
  20.159 -      loop {
  20.160 -        react {
  20.161 -          case Cache_String(x, f) => f(cache_string(x))
  20.162 -          case Cache_Markup(x, f) => f(cache_markup(x))
  20.163 -          case Cache_Tree(x, f) => f(cache_tree(x))
  20.164 -          case Cache_Body(x, f) => f(cache_body(x))
  20.165 -          case Cache_Ignore(x, f) => f(x)
  20.166 -          case bad => System.err.println("XML.cache_actor: ignoring bad input " + bad)
  20.167 -        }
  20.168 -      }
  20.169 -    }
  20.170 -
  20.171 -    private case class Cache_String(x: String, f: String => Unit)
  20.172 -    private case class Cache_Markup(x: Markup, f: Markup => Unit)
  20.173 -    private case class Cache_Tree(x: XML.Tree, f: XML.Tree => Unit)
  20.174 -    private case class Cache_Body(x: XML.Body, f: XML.Body => Unit)
  20.175 -    private case class Cache_Ignore[A](x: A, f: A => Unit)
  20.176 -
  20.177 -    // main methods
  20.178 -    def cache_string(x: String)(f: String => Unit) { cache_actor ! Cache_String(x, f) }
  20.179 -    def cache_markup(x: Markup)(f: Markup => Unit) { cache_actor ! Cache_Markup(x, f) }
  20.180 -    def cache_tree(x: XML.Tree)(f: XML.Tree => Unit) { cache_actor ! Cache_Tree(x, f) }
  20.181 -    def cache_body(x: XML.Body)(f: XML.Body => Unit) { cache_actor ! Cache_Body(x, f) }
  20.182 -    def cache_ignore[A](x: A)(f: A => Unit) { cache_actor ! Cache_Ignore(x, f) }
  20.183 -  }
  20.184 -
  20.185 -
  20.186 -
  20.187 -  /** document object model (W3C DOM) **/
  20.188 -
  20.189 -  def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
  20.190 -    node.getUserData(Markup.Data.name) match {
  20.191 -      case tree: XML.Tree => Some(tree)
  20.192 -      case _ => None
  20.193 -    }
  20.194 -
  20.195 -  def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
  20.196 -  {
  20.197 -    def DOM(tr: Tree): org.w3c.dom.Node = tr match {
  20.198 -      case Elem(Markup.Data, List(data, t)) =>
  20.199 -        val node = DOM(t)
  20.200 -        node.setUserData(Markup.Data.name, data, null)
  20.201 -        node
  20.202 -      case Elem(Markup(name, atts), ts) =>
  20.203 -        if (name == Markup.Data.name)
  20.204 -          error("Malformed data element: " + tr.toString)
  20.205 -        val node = doc.createElement(name)
  20.206 -        for ((name, value) <- atts) node.setAttribute(name, value)
  20.207 -        for (t <- ts) node.appendChild(DOM(t))
  20.208 -        node
  20.209 -      case Text(txt) => doc.createTextNode(txt)
  20.210 -    }
  20.211 -    DOM(tree)
  20.212 -  }
  20.213 -
  20.214 -
  20.215 -
  20.216 -  /** XML as data representation language **/
  20.217 -
  20.218 -  class XML_Atom(s: String) extends Exception(s)
  20.219 -  class XML_Body(body: XML.Body) extends Exception
  20.220 -
  20.221 -  object Encode
  20.222 -  {
  20.223 -    type T[A] = A => XML.Body
  20.224 -
  20.225 -
  20.226 -    /* atomic values */
  20.227 -
  20.228 -    def long_atom(i: Long): String = i.toString
  20.229 -
  20.230 -    def int_atom(i: Int): String = i.toString
  20.231 -
  20.232 -    def bool_atom(b: Boolean): String = if (b) "1" else "0"
  20.233 -
  20.234 -    def unit_atom(u: Unit) = ""
  20.235 -
  20.236 -
  20.237 -    /* structural nodes */
  20.238 -
  20.239 -    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
  20.240 -
  20.241 -    private def vector(xs: List[String]): XML.Attributes =
  20.242 -      xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
  20.243 -
  20.244 -    private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
  20.245 -      XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
  20.246 -
  20.247 -
  20.248 -    /* representation of standard types */
  20.249 -
  20.250 -    val properties: T[Properties.T] =
  20.251 -      (props => List(XML.Elem(Markup(":", props), Nil)))
  20.252 -
  20.253 -    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
  20.254 -
  20.255 -    val long: T[Long] = (x => string(long_atom(x)))
  20.256 -
  20.257 -    val int: T[Int] = (x => string(int_atom(x)))
  20.258 -
  20.259 -    val bool: T[Boolean] = (x => string(bool_atom(x)))
  20.260 -
  20.261 -    val unit: T[Unit] = (x => string(unit_atom(x)))
  20.262 -
  20.263 -    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
  20.264 -      (x => List(node(f(x._1)), node(g(x._2))))
  20.265 -
  20.266 -    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
  20.267 -      (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
  20.268 -
  20.269 -    def list[A](f: T[A]): T[List[A]] =
  20.270 -      (xs => xs.map((x: A) => node(f(x))))
  20.271 -
  20.272 -    def option[A](f: T[A]): T[Option[A]] =
  20.273 -    {
  20.274 -      case None => Nil
  20.275 -      case Some(x) => List(node(f(x)))
  20.276 -    }
  20.277 -
  20.278 -    def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
  20.279 -    {
  20.280 -      case x =>
  20.281 -        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
  20.282 -        List(tagged(tag, f(x)))
  20.283 -    }
  20.284 -  }
  20.285 -
  20.286 -  object Decode
  20.287 -  {
  20.288 -    type T[A] = XML.Body => A
  20.289 -    type V[A] = (List[String], XML.Body) => A
  20.290 -
  20.291 -
  20.292 -    /* atomic values */
  20.293 -
  20.294 -    def long_atom(s: String): Long =
  20.295 -      try { java.lang.Long.parseLong(s) }
  20.296 -      catch { case e: NumberFormatException => throw new XML_Atom(s) }
  20.297 -
  20.298 -    def int_atom(s: String): Int =
  20.299 -      try { Integer.parseInt(s) }
  20.300 -      catch { case e: NumberFormatException => throw new XML_Atom(s) }
  20.301 -
  20.302 -    def bool_atom(s: String): Boolean =
  20.303 -      if (s == "1") true
  20.304 -      else if (s == "0") false
  20.305 -      else throw new XML_Atom(s)
  20.306 -
  20.307 -    def unit_atom(s: String): Unit =
  20.308 -      if (s == "") () else throw new XML_Atom(s)
  20.309 -
  20.310 -
  20.311 -    /* structural nodes */
  20.312 -
  20.313 -    private def node(t: XML.Tree): XML.Body =
  20.314 -      t match {
  20.315 -        case XML.Elem(Markup(":", Nil), ts) => ts
  20.316 -        case _ => throw new XML_Body(List(t))
  20.317 -      }
  20.318 -
  20.319 -    private def vector(atts: XML.Attributes): List[String] =
  20.320 -    {
  20.321 -      val xs = new mutable.ListBuffer[String]
  20.322 -      var i = 0
  20.323 -      for ((a, x) <- atts) {
  20.324 -        if (int_atom(a) == i) { xs += x; i = i + 1 }
  20.325 -        else throw new XML_Atom(a)
  20.326 -      }
  20.327 -      xs.toList
  20.328 -    }
  20.329 -
  20.330 -    private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
  20.331 -      t match {
  20.332 -        case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
  20.333 -        case _ => throw new XML_Body(List(t))
  20.334 -      }
  20.335 -
  20.336 -
  20.337 -    /* representation of standard types */
  20.338 -
  20.339 -    val properties: T[Properties.T] =
  20.340 -    {
  20.341 -      case List(XML.Elem(Markup(":", props), Nil)) => props
  20.342 -      case ts => throw new XML_Body(ts)
  20.343 -    }
  20.344 -
  20.345 -    val string: T[String] =
  20.346 -    {
  20.347 -      case Nil => ""
  20.348 -      case List(XML.Text(s)) => s
  20.349 -      case ts => throw new XML_Body(ts)
  20.350 -    }
  20.351 -
  20.352 -    val long: T[Long] = (x => long_atom(string(x)))
  20.353 -
  20.354 -    val int: T[Int] = (x => int_atom(string(x)))
  20.355 -
  20.356 -    val bool: T[Boolean] = (x => bool_atom(string(x)))
  20.357 -
  20.358 -    val unit: T[Unit] = (x => unit_atom(string(x)))
  20.359 -
  20.360 -    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
  20.361 -    {
  20.362 -      case List(t1, t2) => (f(node(t1)), g(node(t2)))
  20.363 -      case ts => throw new XML_Body(ts)
  20.364 -    }
  20.365 -
  20.366 -    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
  20.367 -    {
  20.368 -      case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
  20.369 -      case ts => throw new XML_Body(ts)
  20.370 -    }
  20.371 -
  20.372 -    def list[A](f: T[A]): T[List[A]] =
  20.373 -      (ts => ts.map(t => f(node(t))))
  20.374 -
  20.375 -    def option[A](f: T[A]): T[Option[A]] =
  20.376 -    {
  20.377 -      case Nil => None
  20.378 -      case List(t) => Some(f(node(t)))
  20.379 -      case ts => throw new XML_Body(ts)
  20.380 -    }
  20.381 -
  20.382 -    def variant[A](fs: List[V[A]]): T[A] =
  20.383 -    {
  20.384 -      case List(t) =>
  20.385 -        val (tag, (xs, ts)) = tagged(t)
  20.386 -        val f =
  20.387 -          try { fs(tag) }
  20.388 -          catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
  20.389 -        f(xs, ts)
  20.390 -      case ts => throw new XML_Body(ts)
  20.391 -    }
  20.392 -  }
  20.393 -}
    21.1 --- a/src/Pure/General/yxml.ML	Mon Sep 05 19:18:38 2011 +0200
    21.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.3 @@ -1,147 +0,0 @@
    21.4 -(*  Title:      Pure/General/yxml.ML
    21.5 -    Author:     Makarius
    21.6 -
    21.7 -Efficient text representation of XML trees using extra characters X
    21.8 -and Y -- no escaping, may nest marked text verbatim.
    21.9 -
   21.10 -Markup <elem att="val" ...>...body...</elem> is encoded as:
   21.11 -
   21.12 -  X Y name Y att=val ... X
   21.13 -  ...
   21.14 -  body
   21.15 -  ...
   21.16 -  X Y X
   21.17 -*)
   21.18 -
   21.19 -signature YXML =
   21.20 -sig
   21.21 -  val X: Symbol.symbol
   21.22 -  val Y: Symbol.symbol
   21.23 -  val embed_controls: string -> string
   21.24 -  val detect: string -> bool
   21.25 -  val output_markup: Markup.T -> string * string
   21.26 -  val element: string -> XML.attributes -> string list -> string
   21.27 -  val string_of_body: XML.body -> string
   21.28 -  val string_of: XML.tree -> string
   21.29 -  val parse_body: string -> XML.body
   21.30 -  val parse: string -> XML.tree
   21.31 -end;
   21.32 -
   21.33 -structure YXML: YXML =
   21.34 -struct
   21.35 -
   21.36 -(** string representation **)
   21.37 -
   21.38 -(* idempotent recoding of certain low ASCII control characters *)
   21.39 -
   21.40 -fun pseudo_utf8 c =
   21.41 -  if Symbol.is_ascii_control c
   21.42 -  then chr 192 ^ chr (128 + ord c)
   21.43 -  else c;
   21.44 -
   21.45 -fun embed_controls str =
   21.46 -  if exists_string Symbol.is_ascii_control str
   21.47 -  then translate_string pseudo_utf8 str
   21.48 -  else str;
   21.49 -
   21.50 -
   21.51 -(* markers *)
   21.52 -
   21.53 -val X = chr 5;
   21.54 -val Y = chr 6;
   21.55 -val XY = X ^ Y;
   21.56 -val XYX = XY ^ X;
   21.57 -
   21.58 -val detect = exists_string (fn s => s = X orelse s = Y);
   21.59 -
   21.60 -
   21.61 -(* output *)
   21.62 -
   21.63 -fun output_markup (markup as (name, atts)) =
   21.64 -  if Markup.is_empty markup then Markup.no_output
   21.65 -  else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
   21.66 -
   21.67 -fun element name atts body =
   21.68 -  let val (pre, post) = output_markup (name, atts)
   21.69 -  in pre ^ implode body ^ post end;
   21.70 -
   21.71 -fun string_of_body body =
   21.72 -  let
   21.73 -    fun attrib (a, x) =
   21.74 -      Buffer.add Y #>
   21.75 -      Buffer.add a #> Buffer.add "=" #> Buffer.add x;
   21.76 -    fun tree (XML.Elem ((name, atts), ts)) =
   21.77 -          Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
   21.78 -          trees ts #>
   21.79 -          Buffer.add XYX
   21.80 -      | tree (XML.Text s) = Buffer.add s
   21.81 -    and trees ts = fold tree ts;
   21.82 -  in Buffer.empty |> trees body |> Buffer.content end;
   21.83 -
   21.84 -val string_of = string_of_body o single;
   21.85 -
   21.86 -
   21.87 -
   21.88 -(** efficient YXML parsing **)
   21.89 -
   21.90 -local
   21.91 -
   21.92 -(* splitting *)
   21.93 -
   21.94 -fun is_char s c = ord s = Char.ord c;
   21.95 -
   21.96 -val split_string =
   21.97 -  Substring.full #>
   21.98 -  Substring.tokens (is_char X) #>
   21.99 -  map (Substring.fields (is_char Y) #> map Substring.string);
  21.100 -
  21.101 -
  21.102 -(* structural errors *)
  21.103 -
  21.104 -fun err msg = raise Fail ("Malformed YXML encoding: " ^ msg);
  21.105 -fun err_attribute () = err "bad attribute";
  21.106 -fun err_element () = err "bad element";
  21.107 -fun err_unbalanced "" = err "unbalanced element"
  21.108 -  | err_unbalanced name = err ("unbalanced element " ^ quote name);
  21.109 -
  21.110 -
  21.111 -(* stack operations *)
  21.112 -
  21.113 -fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending;
  21.114 -
  21.115 -fun push "" _ _ = err_element ()
  21.116 -  | push name atts pending = ((name, atts), []) :: pending;
  21.117 -
  21.118 -fun pop ((("", _), _) :: _) = err_unbalanced ""
  21.119 -  | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
  21.120 -
  21.121 -
  21.122 -(* parsing *)
  21.123 -
  21.124 -fun parse_attrib s =
  21.125 -  (case first_field "=" s of
  21.126 -    NONE => err_attribute ()
  21.127 -  | SOME ("", _) => err_attribute ()
  21.128 -  | SOME att => att);
  21.129 -
  21.130 -fun parse_chunk ["", ""] = pop
  21.131 -  | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
  21.132 -  | parse_chunk txts = fold (add o XML.Text) txts;
  21.133 -
  21.134 -in
  21.135 -
  21.136 -fun parse_body source =
  21.137 -  (case fold parse_chunk (split_string source) [(("", []), [])] of
  21.138 -    [(("", _), result)] => rev result
  21.139 -  | ((name, _), _) :: _ => err_unbalanced name);
  21.140 -
  21.141 -fun parse source =
  21.142 -  (case parse_body source of
  21.143 -    [result] => result
  21.144 -  | [] => XML.Text ""
  21.145 -  | _ => err "multiple results");
  21.146 -
  21.147 -end;
  21.148 -
  21.149 -end;
  21.150 -
    22.1 --- a/src/Pure/General/yxml.scala	Mon Sep 05 19:18:38 2011 +0200
    22.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.3 @@ -1,134 +0,0 @@
    22.4 -/*  Title:      Pure/General/yxml.scala
    22.5 -    Author:     Makarius
    22.6 -
    22.7 -Efficient text representation of XML trees.
    22.8 -*/
    22.9 -
   22.10 -package isabelle
   22.11 -
   22.12 -
   22.13 -import scala.collection.mutable
   22.14 -
   22.15 -
   22.16 -object YXML
   22.17 -{
   22.18 -  /* chunk markers */
   22.19 -
   22.20 -  val X = '\5'
   22.21 -  val Y = '\6'
   22.22 -  val X_string = X.toString
   22.23 -  val Y_string = Y.toString
   22.24 -
   22.25 -  def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
   22.26 -
   22.27 -
   22.28 -  /* string representation */  // FIXME byte array version with pseudo-utf-8 (!?)
   22.29 -
   22.30 -  def string_of_body(body: XML.Body): String =
   22.31 -  {
   22.32 -    val s = new StringBuilder
   22.33 -    def attrib(p: (String, String)) { s += Y; s ++= p._1; s += '='; s ++= p._2 }
   22.34 -    def tree(t: XML.Tree): Unit =
   22.35 -      t match {
   22.36 -        case XML.Elem(Markup(name, atts), ts) =>
   22.37 -          s += X; s += Y; s++= name; atts.foreach(attrib); s += X
   22.38 -          ts.foreach(tree)
   22.39 -          s += X; s += Y; s += X
   22.40 -        case XML.Text(text) => s ++= text
   22.41 -      }
   22.42 -    body.foreach(tree)
   22.43 -    s.toString
   22.44 -  }
   22.45 -
   22.46 -  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
   22.47 -
   22.48 -
   22.49 -  /* parsing */
   22.50 -
   22.51 -  private def err(msg: String) = error("Malformed YXML: " + msg)
   22.52 -  private def err_attribute() = err("bad attribute")
   22.53 -  private def err_element() = err("bad element")
   22.54 -  private def err_unbalanced(name: String) =
   22.55 -    if (name == "") err("unbalanced element")
   22.56 -    else err("unbalanced element " + quote(name))
   22.57 -
   22.58 -  private def parse_attrib(source: CharSequence) = {
   22.59 -    val s = source.toString
   22.60 -    val i = s.indexOf('=')
   22.61 -    if (i <= 0) err_attribute()
   22.62 -    (s.substring(0, i), s.substring(i + 1))
   22.63 -  }
   22.64 -
   22.65 -
   22.66 -  def parse_body(source: CharSequence): XML.Body =
   22.67 -  {
   22.68 -    /* stack operations */
   22.69 -
   22.70 -    def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
   22.71 -    var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
   22.72 -
   22.73 -    def add(x: XML.Tree)
   22.74 -    {
   22.75 -      (stack: @unchecked) match { case ((_, body) :: _) => body += x }
   22.76 -    }
   22.77 -
   22.78 -    def push(name: String, atts: XML.Attributes)
   22.79 -    {
   22.80 -      if (name == "") err_element()
   22.81 -      else stack = (Markup(name, atts), buffer()) :: stack
   22.82 -    }
   22.83 -
   22.84 -    def pop()
   22.85 -    {
   22.86 -      (stack: @unchecked) match {
   22.87 -        case ((Markup.Empty, _) :: _) => err_unbalanced("")
   22.88 -        case ((markup, body) :: pending) =>
   22.89 -          stack = pending
   22.90 -          add(XML.Elem(markup, body.toList))
   22.91 -      }
   22.92 -    }
   22.93 -
   22.94 -
   22.95 -    /* parse chunks */
   22.96 -
   22.97 -    for (chunk <- Library.chunks(source, X) if chunk.length != 0) {
   22.98 -      if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
   22.99 -      else {
  22.100 -        Library.chunks(chunk, Y).toList match {
  22.101 -          case ch :: name :: atts if ch.length == 0 =>
  22.102 -            push(name.toString, atts.map(parse_attrib))
  22.103 -          case txts => for (txt <- txts) add(XML.Text(txt.toString))
  22.104 -        }
  22.105 -      }
  22.106 -    }
  22.107 -    (stack: @unchecked) match {
  22.108 -      case List((Markup.Empty, body)) => body.toList
  22.109 -      case (Markup(name, _), _) :: _ => err_unbalanced(name)
  22.110 -    }
  22.111 -  }
  22.112 -
  22.113 -  def parse(source: CharSequence): XML.Tree =
  22.114 -    parse_body(source) match {
  22.115 -      case List(result) => result
  22.116 -      case Nil => XML.Text("")
  22.117 -      case _ => err("multiple results")
  22.118 -    }
  22.119 -
  22.120 -
  22.121 -  /* failsafe parsing */
  22.122 -
  22.123 -  private def markup_malformed(source: CharSequence) =
  22.124 -    XML.elem(Markup.MALFORMED, List(XML.Text(source.toString)))
  22.125 -
  22.126 -  def parse_body_failsafe(source: CharSequence): XML.Body =
  22.127 -  {
  22.128 -    try { parse_body(source) }
  22.129 -    catch { case ERROR(_) => List(markup_malformed(source)) }
  22.130 -  }
  22.131 -
  22.132 -  def parse_failsafe(source: CharSequence): XML.Tree =
  22.133 -  {
  22.134 -    try { parse(source) }
  22.135 -    catch { case ERROR(_) => markup_malformed(source) }
  22.136 -  }
  22.137 -}
    23.1 --- a/src/Pure/IsaMakefile	Mon Sep 05 19:18:38 2011 +0200
    23.2 +++ b/src/Pure/IsaMakefile	Tue Sep 06 07:23:45 2011 +0200
    23.3 @@ -105,8 +105,6 @@
    23.4    General/table.ML					\
    23.5    General/timing.ML					\
    23.6    General/url.ML					\
    23.7 -  General/xml.ML					\
    23.8 -  General/yxml.ML					\
    23.9    Isar/args.ML						\
   23.10    Isar/attrib.ML					\
   23.11    Isar/auto_bind.ML					\
   23.12 @@ -158,6 +156,8 @@
   23.13    ML/ml_thms.ML						\
   23.14    PIDE/document.ML					\
   23.15    PIDE/isar_document.ML					\
   23.16 +  PIDE/xml.ML						\
   23.17 +  PIDE/yxml.ML						\
   23.18    Proof/extraction.ML					\
   23.19    Proof/proof_checker.ML				\
   23.20    Proof/proof_rewrite_rules.ML				\
    24.1 --- a/src/Pure/ML/ml_lex.ML	Mon Sep 05 19:18:38 2011 +0200
    24.2 +++ b/src/Pure/ML/ml_lex.ML	Tue Sep 06 07:23:45 2011 +0200
    24.3 @@ -106,8 +106,8 @@
    24.4  
    24.5  val token_kind_markup =
    24.6   fn Keyword   => Markup.ML_keyword
    24.7 -  | Ident     => Markup.ML_ident
    24.8 -  | LongIdent => Markup.ML_ident
    24.9 +  | Ident     => Markup.empty
   24.10 +  | LongIdent => Markup.empty
   24.11    | TypeVar   => Markup.ML_tvar
   24.12    | Word      => Markup.ML_numeral
   24.13    | Int       => Markup.ML_numeral
    25.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.2 +++ b/src/Pure/PIDE/xml.ML	Tue Sep 06 07:23:45 2011 +0200
    25.3 @@ -0,0 +1,363 @@
    25.4 +(*  Title:      Pure/PIDE/xml.ML
    25.5 +    Author:     David Aspinall
    25.6 +    Author:     Stefan Berghofer
    25.7 +    Author:     Makarius
    25.8 +
    25.9 +Untyped XML trees and basic data representation.
   25.10 +*)
   25.11 +
   25.12 +signature XML_DATA_OPS =
   25.13 +sig
   25.14 +  type 'a A
   25.15 +  type 'a T
   25.16 +  type 'a V
   25.17 +  val int_atom: int A
   25.18 +  val bool_atom: bool A
   25.19 +  val unit_atom: unit A
   25.20 +  val properties: Properties.T T
   25.21 +  val string: string T
   25.22 +  val int: int T
   25.23 +  val bool: bool T
   25.24 +  val unit: unit T
   25.25 +  val pair: 'a T -> 'b T -> ('a * 'b) T
   25.26 +  val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
   25.27 +  val list: 'a T -> 'a list T
   25.28 +  val option: 'a T -> 'a option T
   25.29 +  val variant: 'a V list -> 'a T
   25.30 +end;
   25.31 +
   25.32 +signature XML =
   25.33 +sig
   25.34 +  type attributes = Properties.T
   25.35 +  datatype tree =
   25.36 +      Elem of Markup.T * tree list
   25.37 +    | Text of string
   25.38 +  type body = tree list
   25.39 +  val add_content: tree -> Buffer.T -> Buffer.T
   25.40 +  val content_of: body -> string
   25.41 +  val header: string
   25.42 +  val text: string -> string
   25.43 +  val element: string -> attributes -> string list -> string
   25.44 +  val output_markup: Markup.T -> Output.output * Output.output
   25.45 +  val string_of: tree -> string
   25.46 +  val pretty: int -> tree -> Pretty.T
   25.47 +  val output: tree -> TextIO.outstream -> unit
   25.48 +  val parse_comments: string list -> unit * string list
   25.49 +  val parse_string : string -> string option
   25.50 +  val parse_element: string list -> tree * string list
   25.51 +  val parse_document: string list -> tree * string list
   25.52 +  val parse: string -> tree
   25.53 +  exception XML_ATOM of string
   25.54 +  exception XML_BODY of body
   25.55 +  structure Encode: XML_DATA_OPS
   25.56 +  structure Decode: XML_DATA_OPS
   25.57 +end;
   25.58 +
   25.59 +structure XML: XML =
   25.60 +struct
   25.61 +
   25.62 +(** XML trees **)
   25.63 +
   25.64 +type attributes = Properties.T;
   25.65 +
   25.66 +datatype tree =
   25.67 +    Elem of Markup.T * tree list
   25.68 +  | Text of string;
   25.69 +
   25.70 +type body = tree list;
   25.71 +
   25.72 +fun add_content (Elem (_, ts)) = fold add_content ts
   25.73 +  | add_content (Text s) = Buffer.add s;
   25.74 +
   25.75 +fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
   25.76 +
   25.77 +
   25.78 +
   25.79 +(** string representation **)
   25.80 +
   25.81 +val header = "<?xml version=\"1.0\"?>\n";
   25.82 +
   25.83 +
   25.84 +(* escaped text *)
   25.85 +
   25.86 +fun decode "&lt;" = "<"
   25.87 +  | decode "&gt;" = ">"
   25.88 +  | decode "&amp;" = "&"
   25.89 +  | decode "&apos;" = "'"
   25.90 +  | decode "&quot;" = "\""
   25.91 +  | decode c = c;
   25.92 +
   25.93 +fun encode "<" = "&lt;"
   25.94 +  | encode ">" = "&gt;"
   25.95 +  | encode "&" = "&amp;"
   25.96 +  | encode "'" = "&apos;"
   25.97 +  | encode "\"" = "&quot;"
   25.98 +  | encode c = c;
   25.99 +
  25.100 +val text = translate_string encode;
  25.101 +
  25.102 +
  25.103 +(* elements *)
  25.104 +
  25.105 +fun elem name atts =
  25.106 +  space_implode " " (name :: map (fn (a, x) => a ^ "=\"" ^ text x ^ "\"") atts);
  25.107 +
  25.108 +fun element name atts body =
  25.109 +  let val b = implode body in
  25.110 +    if b = "" then enclose "<" "/>" (elem name atts)
  25.111 +    else enclose "<" ">" (elem name atts) ^ b ^ enclose "</" ">" name
  25.112 +  end;
  25.113 +
  25.114 +fun output_markup (markup as (name, atts)) =
  25.115 +  if Markup.is_empty markup then Markup.no_output
  25.116 +  else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
  25.117 +
  25.118 +
  25.119 +(* output *)
  25.120 +
  25.121 +fun buffer_of depth tree =
  25.122 +  let
  25.123 +    fun traverse _ (Elem ((name, atts), [])) =
  25.124 +          Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
  25.125 +      | traverse d (Elem ((name, atts), ts)) =
  25.126 +          Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
  25.127 +          traverse_body d ts #>
  25.128 +          Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
  25.129 +      | traverse _ (Text s) = Buffer.add (text s)
  25.130 +    and traverse_body 0 _ = Buffer.add "..."
  25.131 +      | traverse_body d ts = fold (traverse (d - 1)) ts;
  25.132 +  in Buffer.empty |> traverse depth tree end;
  25.133 +
  25.134 +val string_of = Buffer.content o buffer_of ~1;
  25.135 +val output = Buffer.output o buffer_of ~1;
  25.136 +
  25.137 +fun pretty depth tree =
  25.138 +  Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
  25.139 +
  25.140 +
  25.141 +
  25.142 +(** XML parsing **)
  25.143 +
  25.144 +local
  25.145 +
  25.146 +fun err msg (xs, _) =
  25.147 +  fn () => "XML parsing error: " ^ msg () ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
  25.148 +
  25.149 +fun ignored _ = [];
  25.150 +
  25.151 +val blanks = Scan.many Symbol.is_blank;
  25.152 +val special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
  25.153 +val regular = Scan.one Symbol.is_regular;
  25.154 +fun regular_except x = Scan.one (fn c => Symbol.is_regular c andalso c <> x);
  25.155 +
  25.156 +val parse_chars = Scan.repeat1 (special || regular_except "<") >> implode;
  25.157 +
  25.158 +val parse_cdata =
  25.159 +  Scan.this_string "<![CDATA[" |--
  25.160 +  (Scan.repeat (Scan.unless (Scan.this_string "]]>") regular) >> implode) --|
  25.161 +  Scan.this_string "]]>";
  25.162 +
  25.163 +val parse_att =
  25.164 +  (Symbol.scan_id --| (blanks -- $$ "=" -- blanks)) --
  25.165 +  (($$ "\"" || $$ "'") :|-- (fn s =>
  25.166 +    (Scan.repeat (special || regular_except s) >> implode) --| $$ s));
  25.167 +
  25.168 +val parse_comment =
  25.169 +  Scan.this_string "<!--" --
  25.170 +  Scan.repeat (Scan.unless (Scan.this_string "-->") regular) --
  25.171 +  Scan.this_string "-->" >> ignored;
  25.172 +
  25.173 +val parse_processing_instruction =
  25.174 +  Scan.this_string "<?" --
  25.175 +  Scan.repeat (Scan.unless (Scan.this_string "?>") regular) --
  25.176 +  Scan.this_string "?>" >> ignored;
  25.177 +
  25.178 +val parse_doctype =
  25.179 +  Scan.this_string "<!DOCTYPE" --
  25.180 +  Scan.repeat (Scan.unless ($$ ">") regular) --
  25.181 +  $$ ">" >> ignored;
  25.182 +
  25.183 +val parse_misc =
  25.184 +  Scan.one Symbol.is_blank >> ignored ||
  25.185 +  parse_processing_instruction ||
  25.186 +  parse_comment;
  25.187 +
  25.188 +val parse_optional_text =
  25.189 +  Scan.optional (parse_chars >> (single o Text)) [];
  25.190 +
  25.191 +fun name_start_char c = Symbol.is_ascii_letter c orelse c = ":" orelse c = "_";
  25.192 +fun name_char c = name_start_char c orelse Symbol.is_ascii_digit c orelse c = "-" orelse c = ".";
  25.193 +val parse_name = Scan.one name_start_char ::: Scan.many name_char;
  25.194 +
  25.195 +in
  25.196 +
  25.197 +val parse_comments =
  25.198 +  blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K ();
  25.199 +
  25.200 +val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode;
  25.201 +
  25.202 +fun parse_content xs =
  25.203 +  (parse_optional_text @@@
  25.204 +    (Scan.repeat
  25.205 +      ((parse_element >> single ||
  25.206 +        parse_cdata >> (single o Text) ||
  25.207 +        parse_processing_instruction ||
  25.208 +        parse_comment)
  25.209 +      @@@ parse_optional_text) >> flat)) xs
  25.210 +
  25.211 +and parse_element xs =
  25.212 +  ($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--
  25.213 +    (fn (name, _) =>
  25.214 +      !! (err (fn () => "Expected > or />"))
  25.215 +       ($$ "/" -- $$ ">" >> ignored ||
  25.216 +        $$ ">" |-- parse_content --|
  25.217 +          !! (err (fn () => "Expected </" ^ implode name ^ ">"))
  25.218 +              ($$ "<" -- $$ "/" -- Scan.this name -- blanks -- $$ ">")))
  25.219 +    >> (fn ((name, atts), body) => Elem ((implode name, atts), body))) xs;
  25.220 +
  25.221 +val parse_document =
  25.222 +  (Scan.repeat parse_misc -- Scan.option parse_doctype -- Scan.repeat parse_misc)
  25.223 +  |-- parse_element;
  25.224 +
  25.225 +fun parse s =
  25.226 +  (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element"))
  25.227 +      (blanks |-- parse_document --| blanks))) (raw_explode s) of
  25.228 +    (x, []) => x
  25.229 +  | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));
  25.230 +
  25.231 +end;
  25.232 +
  25.233 +
  25.234 +
  25.235 +(** XML as data representation language **)
  25.236 +
  25.237 +exception XML_ATOM of string;
  25.238 +exception XML_BODY of tree list;
  25.239 +
  25.240 +
  25.241 +structure Encode =
  25.242 +struct
  25.243 +
  25.244 +type 'a A = 'a -> string;
  25.245 +type 'a T = 'a -> body;
  25.246 +type 'a V = 'a -> string list * body;
  25.247 +
  25.248 +
  25.249 +(* atomic values *)
  25.250 +
  25.251 +fun int_atom i = signed_string_of_int i;
  25.252 +
  25.253 +fun bool_atom false = "0"
  25.254 +  | bool_atom true = "1";
  25.255 +
  25.256 +fun unit_atom () = "";
  25.257 +
  25.258 +
  25.259 +(* structural nodes *)
  25.260 +
  25.261 +fun node ts = Elem ((":", []), ts);
  25.262 +
  25.263 +fun vector xs = map_index (fn (i, x) => (int_atom i, x)) xs;
  25.264 +
  25.265 +fun tagged (tag, (xs, ts)) = Elem ((int_atom tag, vector xs), ts);
  25.266 +
  25.267 +
  25.268 +(* representation of standard types *)
  25.269 +
  25.270 +fun properties props = [Elem ((":", props), [])];
  25.271 +
  25.272 +fun string "" = []
  25.273 +  | string s = [Text s];
  25.274 +
  25.275 +val int = string o int_atom;
  25.276 +
  25.277 +val bool = string o bool_atom;
  25.278 +
  25.279 +val unit = string o unit_atom;
  25.280 +
  25.281 +fun pair f g (x, y) = [node (f x), node (g y)];
  25.282 +
  25.283 +fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
  25.284 +
  25.285 +fun list f xs = map (node o f) xs;
  25.286 +
  25.287 +fun option _ NONE = []
  25.288 +  | option f (SOME x) = [node (f x)];
  25.289 +
  25.290 +fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
  25.291 +
  25.292 +end;
  25.293 +
  25.294 +
  25.295 +structure Decode =
  25.296 +struct
  25.297 +
  25.298 +type 'a A = string -> 'a;
  25.299 +type 'a T = body -> 'a;
  25.300 +type 'a V = string list * body -> 'a;
  25.301 +
  25.302 +
  25.303 +(* atomic values *)
  25.304 +
  25.305 +fun int_atom s =
  25.306 +  Markup.parse_int s
  25.307 +    handle Fail _ => raise XML_ATOM s;
  25.308 +
  25.309 +fun bool_atom "0" = false
  25.310 +  | bool_atom "1" = true
  25.311 +  | bool_atom s = raise XML_ATOM s;
  25.312 +
  25.313 +fun unit_atom "" = ()
  25.314 +  | unit_atom s = raise XML_ATOM s;
  25.315 +
  25.316 +
  25.317 +(* structural nodes *)
  25.318 +
  25.319 +fun node (Elem ((":", []), ts)) = ts
  25.320 +  | node t = raise XML_BODY [t];
  25.321 +
  25.322 +fun vector atts =
  25.323 +  #1 (fold_map (fn (a, x) =>
  25.324 +        fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts 0);
  25.325 +
  25.326 +fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
  25.327 +  | tagged t = raise XML_BODY [t];
  25.328 +
  25.329 +
  25.330 +(* representation of standard types *)
  25.331 +
  25.332 +fun properties [Elem ((":", props), [])] = props
  25.333 +  | properties ts = raise XML_BODY ts;
  25.334 +
  25.335 +fun string [] = ""
  25.336 +  | string [Text s] = s
  25.337 +  | string ts = raise XML_BODY ts;
  25.338 +
  25.339 +val int = int_atom o string;
  25.340 +
  25.341 +val bool = bool_atom o string;
  25.342 +
  25.343 +val unit = unit_atom o string;
  25.344 +
  25.345 +fun pair f g [t1, t2] = (f (node t1), g (node t2))
  25.346 +  | pair _ _ ts = raise XML_BODY ts;
  25.347 +
  25.348 +fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
  25.349 +  | triple _ _ _ ts = raise XML_BODY ts;
  25.350 +
  25.351 +fun list f ts = map (f o node) ts;
  25.352 +
  25.353 +fun option _ [] = NONE
  25.354 +  | option f [t] = SOME (f (node t))
  25.355 +  | option _ ts = raise XML_BODY ts;
  25.356 +
  25.357 +fun variant fs [t] =
  25.358 +      let
  25.359 +        val (tag, (xs, ts)) = tagged t;
  25.360 +        val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
  25.361 +      in f (xs, ts) end
  25.362 +  | variant _ ts = raise XML_BODY ts;
  25.363 +
  25.364 +end;
  25.365 +
  25.366 +end;
    26.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.2 +++ b/src/Pure/PIDE/xml.scala	Tue Sep 06 07:23:45 2011 +0200
    26.3 @@ -0,0 +1,368 @@
    26.4 +/*  Title:      Pure/PIDE/xml.scala
    26.5 +    Author:     Makarius
    26.6 +
    26.7 +Untyped XML trees and basic data representation.
    26.8 +*/
    26.9 +
   26.10 +package isabelle
   26.11 +
   26.12 +import java.lang.System
   26.13 +import java.util.WeakHashMap
   26.14 +import java.lang.ref.WeakReference
   26.15 +import javax.xml.parsers.DocumentBuilderFactory
   26.16 +
   26.17 +import scala.actors.Actor._
   26.18 +import scala.collection.mutable
   26.19 +
   26.20 +
   26.21 +object XML
   26.22 +{
   26.23 +  /** XML trees **/
   26.24 +
   26.25 +  /* datatype representation */
   26.26 +
   26.27 +  type Attributes = Properties.T
   26.28 +
   26.29 +  sealed abstract class Tree { override def toString = string_of_tree(this) }
   26.30 +  case class Elem(markup: Markup, body: List[Tree]) extends Tree
   26.31 +  case class Text(content: String) extends Tree
   26.32 +
   26.33 +  def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
   26.34 +  def elem(name: String) = Elem(Markup(name, Nil), Nil)
   26.35 +
   26.36 +  type Body = List[Tree]
   26.37 +
   26.38 +
   26.39 +  /* string representation */
   26.40 +
   26.41 +  def string_of_body(body: Body): String =
   26.42 +  {
   26.43 +    val s = new StringBuilder
   26.44 +
   26.45 +    def text(txt: String) {
   26.46 +      if (txt == null) s ++= txt
   26.47 +      else {
   26.48 +        for (c <- txt.iterator) c match {
   26.49 +          case '<' => s ++= "&lt;"
   26.50 +          case '>' => s ++= "&gt;"
   26.51 +          case '&' => s ++= "&amp;"
   26.52 +          case '"' => s ++= "&quot;"
   26.53 +          case '\'' => s ++= "&apos;"
   26.54 +          case _ => s += c
   26.55 +        }
   26.56 +      }
   26.57 +    }
   26.58 +    def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
   26.59 +    def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
   26.60 +    def tree(t: Tree): Unit =
   26.61 +      t match {
   26.62 +        case Elem(markup, Nil) =>
   26.63 +          s ++= "<"; elem(markup); s ++= "/>"
   26.64 +        case Elem(markup, ts) =>
   26.65 +          s ++= "<"; elem(markup); s ++= ">"
   26.66 +          ts.foreach(tree)
   26.67 +          s ++= "</"; s ++= markup.name; s ++= ">"
   26.68 +        case Text(txt) => text(txt)
   26.69 +      }
   26.70 +    body.foreach(tree)
   26.71 +    s.toString
   26.72 +  }
   26.73 +
   26.74 +  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
   26.75 +
   26.76 +
   26.77 +  /* text content */
   26.78 +
   26.79 +  def content_stream(tree: Tree): Stream[String] =
   26.80 +    tree match {
   26.81 +      case Elem(_, body) => content_stream(body)
   26.82 +      case Text(content) => Stream(content)
   26.83 +    }
   26.84 +  def content_stream(body: Body): Stream[String] =
   26.85 +    body.toStream.flatten(content_stream(_))
   26.86 +
   26.87 +  def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
   26.88 +  def content(body: Body): Iterator[String] = content_stream(body).iterator
   26.89 +
   26.90 +
   26.91 +  /* pipe-lined cache for partial sharing */
   26.92 +
   26.93 +  class Cache(initial_size: Int = 131071, max_string: Int = 100)
   26.94 +  {
   26.95 +    private var table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
   26.96 +
   26.97 +    private def lookup[A](x: A): Option[A] =
   26.98 +    {
   26.99 +      val ref = table.get(x)
  26.100 +      if (ref == null) None
  26.101 +      else {
  26.102 +        val y = ref.asInstanceOf[WeakReference[A]].get
  26.103 +        if (y == null) None
  26.104 +        else Some(y)
  26.105 +      }
  26.106 +    }
  26.107 +    private def store[A](x: A): A =
  26.108 +    {
  26.109 +      table.put(x, new WeakReference[Any](x))
  26.110 +      x
  26.111 +    }
  26.112 +
  26.113 +    private def trim_bytes(s: String): String = new String(s.toCharArray)
  26.114 +
  26.115 +    private def _cache_string(x: String): String =
  26.116 +      lookup(x) match {
  26.117 +        case Some(y) => y
  26.118 +        case None =>
  26.119 +          val z = trim_bytes(x)
  26.120 +          if (z.length > max_string) z else store(z)
  26.121 +      }
  26.122 +    private def _cache_props(x: Properties.T): Properties.T =
  26.123 +      if (x.isEmpty) x
  26.124 +      else
  26.125 +        lookup(x) match {
  26.126 +          case Some(y) => y
  26.127 +          case None => store(x.map(p => (trim_bytes(p._1).intern, _cache_string(p._2))))
  26.128 +        }
  26.129 +    private def _cache_markup(x: Markup): Markup =
  26.130 +      lookup(x) match {
  26.131 +        case Some(y) => y
  26.132 +        case None =>
  26.133 +          x match {
  26.134 +            case Markup(name, props) =>
  26.135 +              store(Markup(_cache_string(name), _cache_props(props)))
  26.136 +          }
  26.137 +      }
  26.138 +    private def _cache_tree(x: XML.Tree): XML.Tree =
  26.139 +      lookup(x) match {
  26.140 +        case Some(y) => y
  26.141 +        case None =>
  26.142 +          x match {
  26.143 +            case XML.Elem(markup, body) =>
  26.144 +              store(XML.Elem(_cache_markup(markup), _cache_body(body)))
  26.145 +            case XML.Text(text) => store(XML.Text(_cache_string(text)))
  26.146 +          }
  26.147 +      }
  26.148 +    private def _cache_body(x: XML.Body): XML.Body =
  26.149 +      if (x.isEmpty) x
  26.150 +      else
  26.151 +        lookup(x) match {
  26.152 +          case Some(y) => y
  26.153 +          case None => x.map(_cache_tree(_))
  26.154 +        }
  26.155 +
  26.156 +    // main methods
  26.157 +    def cache_string(x: String): String = synchronized { _cache_string(x) }
  26.158 +    def cache_markup(x: Markup): Markup = synchronized { _cache_markup(x) }
  26.159 +    def cache_tree(x: XML.Tree): XML.Tree = synchronized { _cache_tree(x) }
  26.160 +    def cache_body(x: XML.Body): XML.Body = synchronized { _cache_body(x) }
  26.161 +  }
  26.162 +
  26.163 +
  26.164 +
  26.165 +  /** document object model (W3C DOM) **/
  26.166 +
  26.167 +  def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
  26.168 +    node.getUserData(Markup.Data.name) match {
  26.169 +      case tree: XML.Tree => Some(tree)
  26.170 +      case _ => None
  26.171 +    }
  26.172 +
  26.173 +  def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
  26.174 +  {
  26.175 +    def DOM(tr: Tree): org.w3c.dom.Node = tr match {
  26.176 +      case Elem(Markup.Data, List(data, t)) =>
  26.177 +        val node = DOM(t)
  26.178 +        node.setUserData(Markup.Data.name, data, null)
  26.179 +        node
  26.180 +      case Elem(Markup(name, atts), ts) =>
  26.181 +        if (name == Markup.Data.name)
  26.182 +          error("Malformed data element: " + tr.toString)
  26.183 +        val node = doc.createElement(name)
  26.184 +        for ((name, value) <- atts) node.setAttribute(name, value)
  26.185 +        for (t <- ts) node.appendChild(DOM(t))
  26.186 +        node
  26.187 +      case Text(txt) => doc.createTextNode(txt)
  26.188 +    }
  26.189 +    DOM(tree)
  26.190 +  }
  26.191 +
  26.192 +
  26.193 +
  26.194 +  /** XML as data representation language **/
  26.195 +
  26.196 +  class XML_Atom(s: String) extends Exception(s)
  26.197 +  class XML_Body(body: XML.Body) extends Exception
  26.198 +
  26.199 +  object Encode
  26.200 +  {
  26.201 +    type T[A] = A => XML.Body
  26.202 +
  26.203 +
  26.204 +    /* atomic values */
  26.205 +
  26.206 +    def long_atom(i: Long): String = i.toString
  26.207 +
  26.208 +    def int_atom(i: Int): String = i.toString
  26.209 +
  26.210 +    def bool_atom(b: Boolean): String = if (b) "1" else "0"
  26.211 +
  26.212 +    def unit_atom(u: Unit) = ""
  26.213 +
  26.214 +
  26.215 +    /* structural nodes */
  26.216 +
  26.217 +    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
  26.218 +
  26.219 +    private def vector(xs: List[String]): XML.Attributes =
  26.220 +      xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
  26.221 +
  26.222 +    private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
  26.223 +      XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
  26.224 +
  26.225 +
  26.226 +    /* representation of standard types */
  26.227 +
  26.228 +    val properties: T[Properties.T] =
  26.229 +      (props => List(XML.Elem(Markup(":", props), Nil)))
  26.230 +
  26.231 +    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
  26.232 +
  26.233 +    val long: T[Long] = (x => string(long_atom(x)))
  26.234 +
  26.235 +    val int: T[Int] = (x => string(int_atom(x)))
  26.236 +
  26.237 +    val bool: T[Boolean] = (x => string(bool_atom(x)))
  26.238 +
  26.239 +    val unit: T[Unit] = (x => string(unit_atom(x)))
  26.240 +
  26.241 +    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
  26.242 +      (x => List(node(f(x._1)), node(g(x._2))))
  26.243 +
  26.244 +    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
  26.245 +      (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
  26.246 +
  26.247 +    def list[A](f: T[A]): T[List[A]] =
  26.248 +      (xs => xs.map((x: A) => node(f(x))))
  26.249 +
  26.250 +    def option[A](f: T[A]): T[Option[A]] =
  26.251 +    {
  26.252 +      case None => Nil
  26.253 +      case Some(x) => List(node(f(x)))
  26.254 +    }
  26.255 +
  26.256 +    def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
  26.257 +    {
  26.258 +      case x =>
  26.259 +        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
  26.260 +        List(tagged(tag, f(x)))
  26.261 +    }
  26.262 +  }
  26.263 +
  26.264 +  object Decode
  26.265 +  {
  26.266 +    type T[A] = XML.Body => A
  26.267 +    type V[A] = (List[String], XML.Body) => A
  26.268 +
  26.269 +
  26.270 +    /* atomic values */
  26.271 +
  26.272 +    def long_atom(s: String): Long =
  26.273 +      try { java.lang.Long.parseLong(s) }
  26.274 +      catch { case e: NumberFormatException => throw new XML_Atom(s) }
  26.275 +
  26.276 +    def int_atom(s: String): Int =
  26.277 +      try { Integer.parseInt(s) }
  26.278 +      catch { case e: NumberFormatException => throw new XML_Atom(s) }
  26.279 +
  26.280 +    def bool_atom(s: String): Boolean =
  26.281 +      if (s == "1") true
  26.282 +      else if (s == "0") false
  26.283 +      else throw new XML_Atom(s)
  26.284 +
  26.285 +    def unit_atom(s: String): Unit =
  26.286 +      if (s == "") () else throw new XML_Atom(s)
  26.287 +
  26.288 +
  26.289 +    /* structural nodes */
  26.290 +
  26.291 +    private def node(t: XML.Tree): XML.Body =
  26.292 +      t match {
  26.293 +        case XML.Elem(Markup(":", Nil), ts) => ts
  26.294 +        case _ => throw new XML_Body(List(t))
  26.295 +      }
  26.296 +
  26.297 +    private def vector(atts: XML.Attributes): List[String] =
  26.298 +    {
  26.299 +      val xs = new mutable.ListBuffer[String]
  26.300 +      var i = 0
  26.301 +      for ((a, x) <- atts) {
  26.302 +        if (int_atom(a) == i) { xs += x; i = i + 1 }
  26.303 +        else throw new XML_Atom(a)
  26.304 +      }
  26.305 +      xs.toList
  26.306 +    }
  26.307 +
  26.308 +    private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
  26.309 +      t match {
  26.310 +        case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
  26.311 +        case _ => throw new XML_Body(List(t))
  26.312 +      }
  26.313 +
  26.314 +
  26.315 +    /* representation of standard types */
  26.316 +
  26.317 +    val properties: T[Properties.T] =
  26.318 +    {
  26.319 +      case List(XML.Elem(Markup(":", props), Nil)) => props
  26.320 +      case ts => throw new XML_Body(ts)
  26.321 +    }
  26.322 +
  26.323 +    val string: T[String] =
  26.324 +    {
  26.325 +      case Nil => ""
  26.326 +      case List(XML.Text(s)) => s
  26.327 +      case ts => throw new XML_Body(ts)
  26.328 +    }
  26.329 +
  26.330 +    val long: T[Long] = (x => long_atom(string(x)))
  26.331 +
  26.332 +    val int: T[Int] = (x => int_atom(string(x)))
  26.333 +
  26.334 +    val bool: T[Boolean] = (x => bool_atom(string(x)))
  26.335 +
  26.336 +    val unit: T[Unit] = (x => unit_atom(string(x)))
  26.337 +
  26.338 +    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
  26.339 +    {
  26.340 +      case List(t1, t2) => (f(node(t1)), g(node(t2)))
  26.341 +      case ts => throw new XML_Body(ts)
  26.342 +    }
  26.343 +
  26.344 +    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
  26.345 +    {
  26.346 +      case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
  26.347 +      case ts => throw new XML_Body(ts)
  26.348 +    }
  26.349 +
  26.350 +    def list[A](f: T[A]): T[List[A]] =
  26.351 +      (ts => ts.map(t => f(node(t))))
  26.352 +
  26.353 +    def option[A](f: T[A]): T[Option[A]] =
  26.354 +    {
  26.355 +      case Nil => None
  26.356 +      case List(t) => Some(f(node(t)))
  26.357 +      case ts => throw new XML_Body(ts)
  26.358 +    }
  26.359 +
  26.360 +    def variant[A](fs: List[V[A]]): T[A] =
  26.361 +    {
  26.362 +      case List(t) =>
  26.363 +        val (tag, (xs, ts)) = tagged(t)
  26.364 +        val f =
  26.365 +          try { fs(tag) }
  26.366 +          catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
  26.367 +        f(xs, ts)
  26.368 +      case ts => throw new XML_Body(ts)
  26.369 +    }
  26.370 +  }
  26.371 +}
    27.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.2 +++ b/src/Pure/PIDE/yxml.ML	Tue Sep 06 07:23:45 2011 +0200
    27.3 @@ -0,0 +1,148 @@
    27.4 +(*  Title:      Pure/PIDE/yxml.ML
    27.5 +    Author:     Makarius
    27.6 +
    27.7 +Efficient text representation of XML trees using extra characters X
    27.8 +and Y -- no escaping, may nest marked text verbatim.  Suitable for
    27.9 +direct inlining into plain text.
   27.10 +
   27.11 +Markup <elem att="val" ...>...body...</elem> is encoded as:
   27.12 +
   27.13 +  X Y name Y att=val ... X
   27.14 +  ...
   27.15 +  body
   27.16 +  ...
   27.17 +  X Y X
   27.18 +*)
   27.19 +
   27.20 +signature YXML =
   27.21 +sig
   27.22 +  val X: Symbol.symbol
   27.23 +  val Y: Symbol.symbol
   27.24 +  val embed_controls: string -> string
   27.25 +  val detect: string -> bool
   27.26 +  val output_markup: Markup.T -> string * string
   27.27 +  val element: string -> XML.attributes -> string list -> string
   27.28 +  val string_of_body: XML.body -> string
   27.29 +  val string_of: XML.tree -> string
   27.30 +  val parse_body: string -> XML.body
   27.31 +  val parse: string -> XML.tree
   27.32 +end;
   27.33 +
   27.34 +structure YXML: YXML =
   27.35 +struct
   27.36 +
   27.37 +(** string representation **)
   27.38 +
   27.39 +(* idempotent recoding of certain low ASCII control characters *)
   27.40 +
   27.41 +fun pseudo_utf8 c =
   27.42 +  if Symbol.is_ascii_control c
   27.43 +  then chr 192 ^ chr (128 + ord c)
   27.44 +  else c;
   27.45 +
   27.46 +fun embed_controls str =
   27.47 +  if exists_string Symbol.is_ascii_control str
   27.48 +  then translate_string pseudo_utf8 str
   27.49 +  else str;
   27.50 +
   27.51 +
   27.52 +(* markers *)
   27.53 +
   27.54 +val X = chr 5;
   27.55 +val Y = chr 6;
   27.56 +val XY = X ^ Y;
   27.57 +val XYX = XY ^ X;
   27.58 +
   27.59 +val detect = exists_string (fn s => s = X orelse s = Y);
   27.60 +
   27.61 +
   27.62 +(* output *)
   27.63 +
   27.64 +fun output_markup (markup as (name, atts)) =
   27.65 +  if Markup.is_empty markup then Markup.no_output
   27.66 +  else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
   27.67 +
   27.68 +fun element name atts body =
   27.69 +  let val (pre, post) = output_markup (name, atts)
   27.70 +  in pre ^ implode body ^ post end;
   27.71 +
   27.72 +fun string_of_body body =
   27.73 +  let
   27.74 +    fun attrib (a, x) =
   27.75 +      Buffer.add Y #>
   27.76 +      Buffer.add a #> Buffer.add "=" #> Buffer.add x;
   27.77 +    fun tree (XML.Elem ((name, atts), ts)) =
   27.78 +          Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
   27.79 +          trees ts #>
   27.80 +          Buffer.add XYX
   27.81 +      | tree (XML.Text s) = Buffer.add s
   27.82 +    and trees ts = fold tree ts;
   27.83 +  in Buffer.empty |> trees body |> Buffer.content end;
   27.84 +
   27.85 +val string_of = string_of_body o single;
   27.86 +
   27.87 +
   27.88 +
   27.89 +(** efficient YXML parsing **)
   27.90 +
   27.91 +local
   27.92 +
   27.93 +(* splitting *)
   27.94 +
   27.95 +fun is_char s c = ord s = Char.ord c;
   27.96 +
   27.97 +val split_string =
   27.98 +  Substring.full #>
   27.99 +  Substring.tokens (is_char X) #>
  27.100 +  map (Substring.fields (is_char Y) #> map Substring.string);
  27.101 +
  27.102 +
  27.103 +(* structural errors *)
  27.104 +
  27.105 +fun err msg = raise Fail ("Malformed YXML encoding: " ^ msg);
  27.106 +fun err_attribute () = err "bad attribute";
  27.107 +fun err_element () = err "bad element";
  27.108 +fun err_unbalanced "" = err "unbalanced element"
  27.109 +  | err_unbalanced name = err ("unbalanced element " ^ quote name);
  27.110 +
  27.111 +
  27.112 +(* stack operations *)
  27.113 +
  27.114 +fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending;
  27.115 +
  27.116 +fun push "" _ _ = err_element ()
  27.117 +  | push name atts pending = ((name, atts), []) :: pending;
  27.118 +
  27.119 +fun pop ((("", _), _) :: _) = err_unbalanced ""
  27.120 +  | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
  27.121 +
  27.122 +
  27.123 +(* parsing *)
  27.124 +
  27.125 +fun parse_attrib s =
  27.126 +  (case first_field "=" s of
  27.127 +    NONE => err_attribute ()
  27.128 +  | SOME ("", _) => err_attribute ()
  27.129 +  | SOME att => att);
  27.130 +
  27.131 +fun parse_chunk ["", ""] = pop
  27.132 +  | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
  27.133 +  | parse_chunk txts = fold (add o XML.Text) txts;
  27.134 +
  27.135 +in
  27.136 +
  27.137 +fun parse_body source =
  27.138 +  (case fold parse_chunk (split_string source) [(("", []), [])] of
  27.139 +    [(("", _), result)] => rev result
  27.140 +  | ((name, _), _) :: _ => err_unbalanced name);
  27.141 +
  27.142 +fun parse source =
  27.143 +  (case parse_body source of
  27.144 +    [result] => result
  27.145 +  | [] => XML.Text ""
  27.146 +  | _ => err "multiple results");
  27.147 +
  27.148 +end;
  27.149 +
  27.150 +end;
  27.151 +
    28.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    28.2 +++ b/src/Pure/PIDE/yxml.scala	Tue Sep 06 07:23:45 2011 +0200
    28.3 @@ -0,0 +1,135 @@
    28.4 +/*  Title:      Pure/PIDE/yxml.scala
    28.5 +    Author:     Makarius
    28.6 +
    28.7 +Efficient text representation of XML trees.  Suitable for direct
    28.8 +inlining into plain text.
    28.9 +*/
   28.10 +
   28.11 +package isabelle
   28.12 +
   28.13 +
   28.14 +import scala.collection.mutable
   28.15 +
   28.16 +
   28.17 +object YXML
   28.18 +{
   28.19 +  /* chunk markers */
   28.20 +
   28.21 +  val X = '\5'
   28.22 +  val Y = '\6'
   28.23 +  val X_string = X.toString
   28.24 +  val Y_string = Y.toString
   28.25 +
   28.26 +  def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
   28.27 +
   28.28 +
   28.29 +  /* string representation */  // FIXME byte array version with pseudo-utf-8 (!?)
   28.30 +
   28.31 +  def string_of_body(body: XML.Body): String =
   28.32 +  {
   28.33 +    val s = new StringBuilder
   28.34 +    def attrib(p: (String, String)) { s += Y; s ++= p._1; s += '='; s ++= p._2 }
   28.35 +    def tree(t: XML.Tree): Unit =
   28.36 +      t match {
   28.37 +        case XML.Elem(Markup(name, atts), ts) =>
   28.38 +          s += X; s += Y; s++= name; atts.foreach(attrib); s += X
   28.39 +          ts.foreach(tree)
   28.40 +          s += X; s += Y; s += X
   28.41 +        case XML.Text(text) => s ++= text
   28.42 +      }
   28.43 +    body.foreach(tree)
   28.44 +    s.toString
   28.45 +  }
   28.46 +
   28.47 +  def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
   28.48 +
   28.49 +
   28.50 +  /* parsing */
   28.51 +
   28.52 +  private def err(msg: String) = error("Malformed YXML: " + msg)
   28.53 +  private def err_attribute() = err("bad attribute")
   28.54 +  private def err_element() = err("bad element")
   28.55 +  private def err_unbalanced(name: String) =
   28.56 +    if (name == "") err("unbalanced element")
   28.57 +    else err("unbalanced element " + quote(name))
   28.58 +
   28.59 +  private def parse_attrib(source: CharSequence) = {
   28.60 +    val s = source.toString
   28.61 +    val i = s.indexOf('=')
   28.62 +    if (i <= 0) err_attribute()
   28.63 +    (s.substring(0, i), s.substring(i + 1))
   28.64 +  }
   28.65 +
   28.66 +
   28.67 +  def parse_body(source: CharSequence): XML.Body =
   28.68 +  {
   28.69 +    /* stack operations */
   28.70 +
   28.71 +    def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
   28.72 +    var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
   28.73 +
   28.74 +    def add(x: XML.Tree)
   28.75 +    {
   28.76 +      (stack: @unchecked) match { case ((_, body) :: _) => body += x }
   28.77 +    }
   28.78 +
   28.79 +    def push(name: String, atts: XML.Attributes)
   28.80 +    {
   28.81 +      if (name == "") err_element()
   28.82 +      else stack = (Markup(name, atts), buffer()) :: stack
   28.83 +    }
   28.84 +
   28.85 +    def pop()
   28.86 +    {
   28.87 +      (stack: @unchecked) match {
   28.88 +        case ((Markup.Empty, _) :: _) => err_unbalanced("")
   28.89 +        case ((markup, body) :: pending) =>
   28.90 +          stack = pending
   28.91 +          add(XML.Elem(markup, body.toList))
   28.92 +      }
   28.93 +    }
   28.94 +
   28.95 +
   28.96 +    /* parse chunks */
   28.97 +
   28.98 +    for (chunk <- Library.chunks(source, X) if chunk.length != 0) {
   28.99 +      if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
  28.100 +      else {
  28.101 +        Library.chunks(chunk, Y).toList match {
  28.102 +          case ch :: name :: atts if ch.length == 0 =>
  28.103 +            push(name.toString, atts.map(parse_attrib))
  28.104 +          case txts => for (txt <- txts) add(XML.Text(txt.toString))
  28.105 +        }
  28.106 +      }
  28.107 +    }
  28.108 +    (stack: @unchecked) match {
  28.109 +      case List((Markup.Empty, body)) => body.toList
  28.110 +      case (Markup(name, _), _) :: _ => err_unbalanced(name)
  28.111 +    }
  28.112 +  }
  28.113 +
  28.114 +  def parse(source: CharSequence): XML.Tree =
  28.115 +    parse_body(source) match {
  28.116 +      case List(result) => result
  28.117 +      case Nil => XML.Text("")
  28.118 +      case _ => err("multiple results")
  28.119 +    }
  28.120 +
  28.121 +
  28.122 +  /* failsafe parsing */
  28.123 +
  28.124 +  private def markup_malformed(source: CharSequence) =
  28.125 +    XML.elem(Markup.MALFORMED, List(XML.Text(source.toString)))
  28.126 +
  28.127 +  def parse_body_failsafe(source: CharSequence): XML.Body =
  28.128 +  {
  28.129 +    try { parse_body(source) }
  28.130 +    catch { case ERROR(_) => List(markup_malformed(source)) }
  28.131 +  }
  28.132 +
  28.133 +  def parse_failsafe(source: CharSequence): XML.Tree =
  28.134 +  {
  28.135 +    try { parse(source) }
  28.136 +    catch { case ERROR(_) => markup_malformed(source) }
  28.137 +  }
  28.138 +}
    29.1 --- a/src/Pure/ROOT.ML	Mon Sep 05 19:18:38 2011 +0200
    29.2 +++ b/src/Pure/ROOT.ML	Tue Sep 06 07:23:45 2011 +0200
    29.3 @@ -54,17 +54,18 @@
    29.4  use "General/linear_set.ML";
    29.5  use "General/buffer.ML";
    29.6  use "General/pretty.ML";
    29.7 -use "General/xml.ML";
    29.8  use "General/path.ML";
    29.9  use "General/url.ML";
   29.10  use "General/file.ML";
   29.11 -use "General/yxml.ML";
   29.12  use "General/long_name.ML";
   29.13  use "General/binding.ML";
   29.14  
   29.15  use "General/sha1.ML";
   29.16  if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
   29.17  
   29.18 +use "PIDE/xml.ML";
   29.19 +use "PIDE/yxml.ML";
   29.20 +
   29.21  
   29.22  (* concurrency within the ML runtime *)
   29.23  
    30.1 --- a/src/Pure/Syntax/lexicon.ML	Mon Sep 05 19:18:38 2011 +0200
    30.2 +++ b/src/Pure/Syntax/lexicon.ML	Tue Sep 06 07:23:45 2011 +0200
    30.3 @@ -190,8 +190,8 @@
    30.4  
    30.5  val token_kind_markup =
    30.6   fn Literal     => Markup.literal
    30.7 -  | IdentSy     => Markup.ident
    30.8 -  | LongIdentSy => Markup.ident
    30.9 +  | IdentSy     => Markup.empty
   30.10 +  | LongIdentSy => Markup.empty
   30.11    | VarSy       => Markup.var
   30.12    | TFreeSy     => Markup.tfree
   30.13    | TVarSy      => Markup.tvar
    31.1 --- a/src/Pure/System/isabelle_process.scala	Mon Sep 05 19:18:38 2011 +0200
    31.2 +++ b/src/Pure/System/isabelle_process.scala	Tue Sep 06 07:23:45 2011 +0200
    31.3 @@ -99,12 +99,10 @@
    31.4    {
    31.5      if (kind == Markup.INIT) rm_fifos()
    31.6      if (kind == Markup.RAW)
    31.7 -      xml_cache.cache_ignore(
    31.8 -        new Result(XML.Elem(Markup(kind, props), body)))((result: Result) => receiver ! result)
    31.9 +      receiver ! new Result(XML.Elem(Markup(kind, props), body))
   31.10      else {
   31.11        val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
   31.12 -      xml_cache.cache_tree(msg)((message: XML.Tree) =>
   31.13 -        receiver ! new Result(message.asInstanceOf[XML.Elem]))
   31.14 +      receiver ! new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem])
   31.15      }
   31.16    }
   31.17  
    32.1 --- a/src/Pure/Thy/thy_syntax.ML	Mon Sep 05 19:18:38 2011 +0200
    32.2 +++ b/src/Pure/Thy/thy_syntax.ML	Tue Sep 06 07:23:45 2011 +0200
    32.3 @@ -45,14 +45,14 @@
    32.4  val token_kind_markup =
    32.5   fn Token.Command       => Markup.command
    32.6    | Token.Keyword       => Markup.keyword
    32.7 -  | Token.Ident         => Markup.ident
    32.8 -  | Token.LongIdent     => Markup.ident
    32.9 -  | Token.SymIdent      => Markup.ident
   32.10 +  | Token.Ident         => Markup.empty
   32.11 +  | Token.LongIdent     => Markup.empty
   32.12 +  | Token.SymIdent      => Markup.empty
   32.13    | Token.Var           => Markup.var
   32.14    | Token.TypeIdent     => Markup.tfree
   32.15    | Token.TypeVar       => Markup.tvar
   32.16 -  | Token.Nat           => Markup.ident
   32.17 -  | Token.Float         => Markup.ident
   32.18 +  | Token.Nat           => Markup.empty
   32.19 +  | Token.Float         => Markup.empty
   32.20    | Token.String        => Markup.string
   32.21    | Token.AltString     => Markup.altstring
   32.22    | Token.Verbatim      => Markup.verbatim
    33.1 --- a/src/Pure/build-jars	Mon Sep 05 19:18:38 2011 +0200
    33.2 +++ b/src/Pure/build-jars	Tue Sep 06 07:23:45 2011 +0200
    33.3 @@ -24,8 +24,6 @@
    33.4    General/scan.scala
    33.5    General/sha1.scala
    33.6    General/symbol.scala
    33.7 -  General/xml.scala
    33.8 -  General/yxml.scala
    33.9    Isar/keyword.scala
   33.10    Isar/outer_syntax.scala
   33.11    Isar/parse.scala
   33.12 @@ -36,6 +34,8 @@
   33.13    PIDE/isar_document.scala
   33.14    PIDE/markup_tree.scala
   33.15    PIDE/text.scala
   33.16 +  PIDE/xml.scala
   33.17 +  PIDE/yxml.scala
   33.18    System/cygwin.scala
   33.19    System/download.scala
   33.20    System/event_bus.scala
    34.1 --- a/src/Tools/jEdit/README	Mon Sep 05 19:18:38 2011 +0200
    34.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    34.3 @@ -1,62 +0,0 @@
    34.4 -Isabelle/jEdit based on Isabelle/Scala
    34.5 -======================================
    34.6 -
    34.7 -The Isabelle/Scala layer that is already part of Isabelle/Pure
    34.8 -provides some general infrastructure for advanced prover interaction
    34.9 -and integration.  The Isabelle/jEdit application serves as an example
   34.10 -for asynchronous proof checking with support for parallel processing.
   34.11 -
   34.12 -See also the paper:
   34.13 -
   34.14 -  Makarius Wenzel. Asynchronous Proof Processing with Isabelle/Scala
   34.15 -  and Isabelle/jEdit. In C. Sacerdoti Coen and D. Aspinall, editors,
   34.16 -  User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite
   34.17 -  Workshop, Edinburgh, Scotland, July 2010. To appear in ENTCS.
   34.18 -  http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf
   34.19 -
   34.20 -
   34.21 -Known problems with Mac OS
   34.22 -==========================
   34.23 -
   34.24 -- The MacOSX plugin for jEdit disrupts regular C-X/C/V operations,
   34.25 -  e.g. between the editor and the Console plugin, which is a standard
   34.26 -  swing text box.  Similar for search boxes etc.
   34.27 -
   34.28 -- ToggleButton selected state is not rendered if window focus is lost,
   34.29 -  which is probably a genuine feature of the Apple look-and-feel.
   34.30 -
   34.31 -- Anti-aliasing does not really work as well as for Linux or Windows.
   34.32 -  (General Apple/Swing problem?)
   34.33 -
   34.34 -- Font.createFont mangles the font family of non-regular fonts,
   34.35 -  e.g. bold.  IsabelleText font files need to be installed manually.
   34.36 -
   34.37 -- Missing glyphs are collected from other fonts (like Emacs, Firefox).
   34.38 -  This is actually an advantage over the Oracle/Sun JVM on Windows or
   34.39 -  Linux, but probably also the deeper reason for the other oddities of
   34.40 -  Apple font management.
   34.41 -
   34.42 -- The native font renderer of -Dapple.awt.graphics.UseQuartz=true
   34.43 -  fails to handle the infinitesimal font size of "hidden" text (e.g.
   34.44 -  used in Isabelle sub/superscripts).
   34.45 -
   34.46 -
   34.47 -Known problems with OpenJDK
   34.48 -===========================
   34.49 -
   34.50 -- The 2D rendering engine of OpenJDK 1.6.x distorts the appearance of
   34.51 -  the jEdit text area.  Always use official JRE 1.6.x from
   34.52 -  Sun/Oracle/Apple.
   34.53 -
   34.54 -
   34.55 -Licenses and home sites of contributing systems
   34.56 -===============================================
   34.57 -
   34.58 -* Scala: BSD-style
   34.59 -  http://www.scala-lang.org
   34.60 -
   34.61 -* jEdit: GPL (with special cases)
   34.62 -  http://www.jedit.org/
   34.63 -
   34.64 -* Lobo/Cobra: GPL and LGPL
   34.65 -  http://lobobrowser.org/
    35.1 --- a/src/Tools/jEdit/README.html	Mon Sep 05 19:18:38 2011 +0200
    35.2 +++ b/src/Tools/jEdit/README.html	Tue Sep 06 07:23:45 2011 +0200
    35.3 @@ -12,7 +12,12 @@
    35.4  
    35.5  <body>
    35.6  
    35.7 -<h2>The Isabelle/jEdit Prover IDE</h2>
    35.8 +<h2>The Isabelle/jEdit Prover IDE (based on Isabelle/Scala)</h2>
    35.9 +
   35.10 +The Isabelle/Scala layer that is already part of Isabelle/Pure
   35.11 +provides some general infrastructure for advanced prover interaction
   35.12 +and integration.  The Isabelle/jEdit application serves as an example
   35.13 +for asynchronous proof checking with support for parallel processing.
   35.14  
   35.15  <ul>
   35.16  
   35.17 @@ -116,30 +121,23 @@
   35.18  </ul>
   35.19  
   35.20  
   35.21 -<h2>Limitations and workrounds (January 2011)</h2>
   35.22 +<h2>Limitations and workrounds (September 2011)</h2>
   35.23  
   35.24  <ul>
   35.25    <li>No way to start/stop prover or switch to a different logic.<br/>
   35.26    <em>Workaround:</em> Change options and restart editor.</li>
   35.27  
   35.28 -  <li>Limited support for dependencies between multiple theory buffers.<br/>
   35.29 -  <em>Workaround:</em> Load required files manually.</li>
   35.30 -
   35.31 -  <li>No reclaiming of old/unused document versions in prover or
   35.32 -  editor.<br/>
   35.33 -  <em>Workaround:</em> Avoid large files; restart after a few hours of use.</li>
   35.34 -
   35.35    <li>Incremental reparsing sometimes produces unexpected command
   35.36    spans.<br/>
   35.37    <em>Workaround:</em> Cut/paste larger parts or reload buffer.</li>
   35.38  
   35.39 -  <li>Command execution sometimes gets stuck (purple background).<br/>
   35.40 -  <em>Workaround:</em> Force reparsing as above.</li>
   35.41 +  <li>Odd behavior of some diagnostic commands, notably those starting
   35.42 +  external processes asynchronously (e.g. <tt>thy_deps</tt>).<br/>
   35.43 +  <em>Workaround:</em> Avoid such commands.</li>
   35.44  
   35.45 -  <li>Odd behavior of some diagnostic commands, notably those
   35.46 -  starting external processes asynchronously
   35.47 -  (e.g. <tt>thy_deps</tt>, <tt>sledgehammer</tt>).<br/>
   35.48 -  <em>Workaround:</em> Avoid such commands.</li>
   35.49 +  <li>Lack of dependency managed for auxiliary files that contribute
   35.50 +  to a theory ("<b>uses</b>").<br/>
   35.51 +  <em>Workaround:</em> Re-use files manually within the prover.</li>
   35.52  
   35.53    <li>No support for non-local markup, e.g. commands reporting on
   35.54    previous commands (proof end on proof head), or markup produced by
   35.55 @@ -149,6 +147,59 @@
   35.56    General.</li>
   35.57  </ul>
   35.58  
   35.59 +
   35.60 +<h2>Known problems with Mac OS</h2>
   35.61 +
   35.62 +<ul>
   35.63 +
   35.64 +<li>The MacOSX plugin for jEdit disrupts regular C-X/C/V operations,
   35.65 +  e.g. between the editor and the Console plugin, which is a standard
   35.66 +  swing text box.  Similar for search boxes etc.</li>
   35.67 +
   35.68 +<li>ToggleButton selected state is not rendered if window focus is
   35.69 +  lost, which is probably a genuine feature of the Apple
   35.70 +  look-and-feel.</li>
   35.71 +
   35.72 +<li>Font.createFont mangles the font family of non-regular fonts,
   35.73 +  e.g. bold.  IsabelleText font files need to be installed/updated
   35.74 +  manually.</li>
   35.75 +
   35.76 +<li>Missing glyphs are collected from other fonts (like Emacs,
   35.77 +  Firefox).  This is actually an advantage over the Oracle/Sun JVM on
   35.78 +  Windows or Linux, but probably also the deeper reason for the other
   35.79 +  oddities of Apple font management.</li>
   35.80 +
   35.81 +<li>The native font renderer of -Dapple.awt.graphics.UseQuartz=true
   35.82 +  (not enabled by default) fails to handle the infinitesimal font size
   35.83 +  of "hidden" text (e.g.  used in Isabelle sub/superscripts).</li>
   35.84 +
   35.85 +</ul>
   35.86 +
   35.87 +
   35.88 +<h2>Known problems with OpenJDK 1.6.x</h2>
   35.89 +
   35.90 +<ul>
   35.91 +
   35.92 +<li>The 2D rendering engine of OpenJDK 1.6.x distorts the appearance
   35.93 +  of the jEdit text area.  Always use official JRE 1.6.x from
   35.94 +  Sun/Oracle/Apple.</li>
   35.95 +
   35.96 +<li>jEdit on OpenJDK is generally not supported.</li>
   35.97 +
   35.98 +</ul>
   35.99 +
  35.100 +
  35.101 +<h2>Licenses and home sites of contributing systems</h2>
  35.102 +
  35.103 +<ul>
  35.104 +
  35.105 +<li>Scala: BSD-style <br/> http://www.scala-lang.org</li>
  35.106 +
  35.107 +<li>jEdit: GPL (with special cases) <br/> http://www.jedit.org/</li>
  35.108 +
  35.109 +<li>Lobo/Cobra: GPL and LGPL <br/> http://lobobrowser.org/</li>
  35.110 +
  35.111 +</ul>
  35.112 +
  35.113  </body>
  35.114  </html>
  35.115 -
    36.1 --- a/src/Tools/jEdit/README_BUILD	Mon Sep 05 19:18:38 2011 +0200
    36.2 +++ b/src/Tools/jEdit/README_BUILD	Tue Sep 06 07:23:45 2011 +0200
    36.3 @@ -1,14 +1,14 @@
    36.4  Requirements for instantaneous build from sources
    36.5  =================================================
    36.6  
    36.7 -* Official Java JDK from Sun/Oracle/Apple, e.g. 1.6.0_26
    36.8 -  http://java.sun.com/javase/downloads/index.jsp
    36.9 +* Official Java JDK from Sun/Oracle/Apple, e.g. 1.6.0_27
   36.10 +  http://www.oracle.com/technetwork/java/javase/downloads/index.html
   36.11  
   36.12  * Scala Compiler 2.8.1.final
   36.13    http://www.scala-lang.org
   36.14  
   36.15  * Auxiliary jedit_build component
   36.16 -  http://www4.in.tum.de/~wenzelm/test/jedit_build-20110521.tar.gz
   36.17 +  http://www4.in.tum.de/~wenzelm/test/jedit_build-20110622.tar.gz
   36.18  
   36.19  
   36.20  Important settings within Isabelle environment
   36.21 @@ -16,7 +16,7 @@
   36.22  
   36.23  - JAVA_HOME
   36.24  - SCALA_HOME
   36.25 -- JEDIT_BUILD_HOME (via "init_component .../jedit_build...")
   36.26 +- ISABELLE_JEDIT_BUILD_HOME (via "init_component .../jedit_build...")
   36.27  
   36.28  
   36.29  Build and run
    37.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Mon Sep 05 19:18:38 2011 +0200
    37.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Tue Sep 06 07:23:45 2011 +0200
    37.3 @@ -128,10 +128,7 @@
    37.4    }
    37.5  
    37.6    private val text_entity_colors: Map[String, Color] =
    37.7 -    Map(
    37.8 -      Markup.CLASS -> get_color("red"),
    37.9 -      Markup.TYPE -> get_color("black"),
   37.10 -      Markup.CONSTANT -> get_color("black"))
   37.11 +    Map(Markup.CLASS -> get_color("red"))
   37.12  
   37.13    private val text_colors: Map[String, Color] =
   37.14      Map(
   37.15 @@ -140,7 +137,6 @@
   37.16        Markup.VERBATIM -> get_color("black"),
   37.17        Markup.LITERAL -> keyword1_color,
   37.18        Markup.DELIMITER -> get_color("black"),
   37.19 -      Markup.IDENT -> get_color("black"),
   37.20        Markup.TFREE -> get_color("#A020F0"),
   37.21        Markup.TVAR -> get_color("#A020F0"),
   37.22        Markup.FREE -> get_color("blue"),
    38.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Mon Sep 05 19:18:38 2011 +0200
    38.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Tue Sep 06 07:23:45 2011 +0200
    38.3 @@ -63,6 +63,6 @@
    38.4        tooltip_margin.getValue().asInstanceOf[Int]
    38.5  
    38.6      Isabelle.Time_Property("tooltip-dismiss-delay") =
    38.7 -      Time.seconds(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
    38.8 +      Time.ms(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
    38.9    }
   38.10  }
    39.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Sep 05 19:18:38 2011 +0200
    39.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Sep 06 07:23:45 2011 +0200
    39.3 @@ -123,8 +123,10 @@
    39.4          Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)
    39.5        HTML.encode(text) + "</pre></html>"
    39.6  
    39.7 +  private val tooltip_lb = Time.seconds(0.5)
    39.8 +  private val tooltip_ub = Time.seconds(60.0)
    39.9    def tooltip_dismiss_delay(): Time =
   39.10 -    Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5)
   39.11 +    Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max tooltip_lb min tooltip_ub
   39.12  
   39.13    def setup_tooltips()
   39.14    {
    40.1 --- a/src/Tools/jEdit/src/token_markup.scala	Mon Sep 05 19:18:38 2011 +0200
    40.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Tue Sep 06 07:23:45 2011 +0200
    40.3 @@ -173,41 +173,42 @@
    40.4            case _ => Some(Scan.Finished)
    40.5          }
    40.6        val context1 =
    40.7 -        if (line_ctxt.isDefined && Isabelle.session.is_ready) {
    40.8 -          val syntax = Isabelle.session.current_syntax()
    40.9 -    
   40.10 -          val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
   40.11 -          val context1 = new Line_Context(Some(ctxt1))
   40.12 -    
   40.13 -          val extended = extended_styles(line)
   40.14 -    
   40.15 -          var offset = 0
   40.16 -          for (token <- tokens) {
   40.17 -            val style = Isabelle_Markup.token_markup(syntax, token)
   40.18 -            val length = token.source.length
   40.19 -            val end_offset = offset + length
   40.20 -            if ((offset until end_offset) exists extended.isDefinedAt) {
   40.21 -              for (i <- offset until end_offset) {
   40.22 -                val style1 =
   40.23 -                  extended.get(i) match {
   40.24 -                    case None => style
   40.25 -                    case Some(ext) => ext(style)
   40.26 -                  }
   40.27 -                handler.handleToken(line, style1, i, 1, context1)
   40.28 -              }
   40.29 +      {
   40.30 +        val (styled_tokens, context1) =
   40.31 +          if (line_ctxt.isDefined && Isabelle.session.is_ready) {
   40.32 +            val syntax = Isabelle.session.current_syntax()
   40.33 +            val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
   40.34 +            val styled_tokens = tokens.map(tok => (Isabelle_Markup.token_markup(syntax, tok), tok))
   40.35 +            (styled_tokens, new Line_Context(Some(ctxt1)))
   40.36 +          }
   40.37 +          else {
   40.38 +            val token = Token(Token.Kind.UNPARSED, line.subSequence(0, line.count).toString)
   40.39 +            (List((JEditToken.NULL, token)), new Line_Context(None))
   40.40 +          }
   40.41 +
   40.42 +        val extended = extended_styles(line)
   40.43 +
   40.44 +        var offset = 0
   40.45 +        for ((style, token) <- styled_tokens) {
   40.46 +          val length = token.source.length
   40.47 +          val end_offset = offset + length
   40.48 +          if ((offset until end_offset) exists
   40.49 +              (i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {
   40.50 +            for (i <- offset until end_offset) {
   40.51 +              val style1 =
   40.52 +                extended.get(i) match {
   40.53 +                  case None => style
   40.54 +                  case Some(ext) => ext(style)
   40.55 +                }
   40.56 +              handler.handleToken(line, style1, i, 1, context1)
   40.57              }
   40.58 -            else handler.handleToken(line, style, offset, length, context1)
   40.59 -            offset += length
   40.60            }
   40.61 -          handler.handleToken(line, JEditToken.END, line.count, 0, context1)
   40.62 -          context1
   40.63 +          else handler.handleToken(line, style, offset, length, context1)
   40.64 +          offset += length
   40.65          }
   40.66 -        else {
   40.67 -          val context1 = new Line_Context(None)
   40.68 -          handler.handleToken(line, JEditToken.NULL, 0, line.count, context1)
   40.69 -          handler.handleToken(line, JEditToken.END, line.count, 0, context1)
   40.70 -          context1
   40.71 -        }
   40.72 +        handler.handleToken(line, JEditToken.END, line.count, 0, context1)
   40.73 +        context1
   40.74 +      }
   40.75        val context2 = context1.intern
   40.76        handler.setLineContext(context2)
   40.77        context2