# HG changeset patch
# User wenzelm
# Date 1393624575 -3600
# Node ID 557003a7cf787830a35d584fd91992df610e767c
# Parent  aa1acc25126b03b104a5c5d2096eb031c047e29e# Parent  aefa1db74d9dfa82b0039a2f66ea129cf9ada816
merged

diff -r aa1acc25126b -r 557003a7cf78 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Fri Feb 28 17:54:52 2014 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Feb 28 22:56:15 2014 +0100
@@ -269,7 +269,7 @@
 lemma numsubst0_numbound0:
   assumes nb: "numbound0 t"
   shows "numbound0 (numsubst0 t a)"
-  using nb apply (induct a) 
+  using nb apply (induct a)
   apply simp_all
   apply (case_tac nat, simp_all)
   done
@@ -2001,8 +2001,9 @@
 oracle linzqe_oracle = {*
 let
 
-fun num_of_term vs (t as Free (xn, xT)) = (case AList.lookup (op =) vs t
-     of NONE => error "Variable not found in the list!"
+fun num_of_term vs (t as Free (xn, xT)) =
+      (case AList.lookup (op =) vs t of
+        NONE => error "Variable not found in the list!"
       | SOME n => @{code Bound} (@{code nat_of_integer} n))
   | num_of_term vs @{term "0::int"} = @{code C} (@{code int_of_integer} 0)
   | num_of_term vs @{term "1::int"} = @{code C} (@{code int_of_integer} 1)
@@ -2018,11 +2019,12 @@
   | num_of_term vs (@{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
       @{code Sub} (num_of_term vs t1, num_of_term vs t2)
   | num_of_term vs (@{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =
-      (case try HOLogic.dest_number t1
-       of SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t2)
-        | NONE => (case try HOLogic.dest_number t2
-                of SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t1)
-                 | NONE => error "num_of_term: unsupported multiplication"))
+      (case try HOLogic.dest_number t1 of
+        SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t2)
+      | NONE =>
+          (case try HOLogic.dest_number t2 of
+            SOME (_, i) => @{code Mul} (@{code int_of_integer} i, num_of_term vs t1)
+          | NONE => error "num_of_term: unsupported multiplication"))
   | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t);
 
 fun fm_of_term ps vs @{term True} = @{code T}
@@ -2034,9 +2036,9 @@
   | fm_of_term ps vs (@{term "op = :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
       @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
   | fm_of_term ps vs (@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"} $ t1 $ t2) =
-      (case try HOLogic.dest_number t1
-       of SOME (_, i) => @{code Dvd} (@{code int_of_integer} i, num_of_term vs t2)
-        | NONE => error "num_of_term: unsupported dvd")
+      (case try HOLogic.dest_number t1 of
+        SOME (_, i) => @{code Dvd} (@{code int_of_integer} i, num_of_term vs t2)
+      | NONE => error "num_of_term: unsupported dvd")
   | fm_of_term ps vs (@{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t1 $ t2) =
       @{code Iff} (fm_of_term ps vs t1, fm_of_term ps vs t2)
   | fm_of_term ps vs (@{term HOL.conj} $ t1 $ t2) =
@@ -2071,7 +2073,8 @@
       term_of_num vs t1 $ term_of_num vs t2
   | term_of_num vs (@{code Mul} (i, t2)) = @{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} $
       term_of_num vs (@{code C} i) $ term_of_num vs t2
-  | term_of_num vs (@{code CN} (n, i, t)) = term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
+  | term_of_num vs (@{code CN} (n, i, t)) =
+      term_of_num vs (@{code Add} (@{code Mul} (i, @{code Bound} n), t));
 
 fun term_of_fm ps vs @{code T} = @{term True}
   | term_of_fm ps vs @{code F} = @{term False}
@@ -2109,30 +2112,36 @@
 
 fun term_bools acc t =
   let
-    val is_op = member (op =) [@{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies}, @{term "op = :: bool => _"},
+    val is_op =
+      member (op =) [@{term HOL.conj}, @{term HOL.disj}, @{term HOL.implies},
+      @{term "op = :: bool => _"},
       @{term "op = :: int => _"}, @{term "op < :: int => _"},
       @{term "op <= :: int => _"}, @{term "Not"}, @{term "All :: (int => _) => _"},
       @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}]
     fun is_ty t = not (fastype_of t = HOLogic.boolT)
-  in case t
-   of (l as f $ a) $ b => if is_ty t orelse is_op t then term_bools (term_bools acc l)b
+  in
+    (case t of
+      (l as f $ a) $ b =>
+        if is_ty t orelse is_op t then term_bools (term_bools acc l) b
         else insert (op aconv) t acc
-    | f $ a => if is_ty t orelse is_op t then term_bools (term_bools acc f) a
+    | f $ a =>
+        if is_ty t orelse is_op t then term_bools (term_bools acc f) a
         else insert (op aconv) t acc
     | Abs p => term_bools acc (snd (Syntax_Trans.variant_abs p))  (* FIXME !? *)
-    | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc
+    | _ => if is_ty t orelse is_op t then acc else insert (op aconv) t acc)
   end;
 
-in fn ct =>
-  let
-    val thy = Thm.theory_of_cterm ct;
-    val t = Thm.term_of ct;
-    val fs = Misc_Legacy.term_frees t;
-    val bs = term_bools [] t;
-    val vs = map_index swap fs;
-    val ps = map_index swap bs;
-    val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t;
-  in (Thm.cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (t, t') end
+in
+  fn ct =>
+    let
+      val thy = Thm.theory_of_cterm ct;
+      val t = Thm.term_of ct;
+      val fs = Misc_Legacy.term_frees t;
+      val bs = term_bools [] t;
+      val vs = map_index swap fs;
+      val ps = map_index swap bs;
+      val t' = (term_of_fm ps vs o @{code pa} o fm_of_term ps vs) t;
+    in Thm.cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) end
 end;
 *}
 
@@ -2146,83 +2155,86 @@
 
 text {* Tests *}
 
-lemma "\<exists>(j::int). \<forall>x\<ge>j. (\<exists>a b. x = 3*a+5*b)"
+lemma "\<exists>(j::int). \<forall>x\<ge>j. \<exists>a b. x = 3*a+5*b"
   by cooper
 
-lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x"
+lemma "\<forall>(x::int) \<ge> 8. \<exists>i j. 5*i + 3*j = x"
   by cooper
 
-theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
+theorem "(\<forall>(y::int). 3 dvd y) \<Longrightarrow> \<forall>(x::int). b < x \<longrightarrow> a \<le> x"
   by cooper
 
-theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==>
-  (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
+theorem "\<And>(y::int) (z::int) (n::int). 3 dvd z \<Longrightarrow> 2 dvd (y::int) \<Longrightarrow>
+    (\<exists>(x::int). 2*x = y) \<and> (\<exists>(k::int). 3*k = z)"
   by cooper
 
-theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==>  3 dvd z ==>
-  2 dvd (y::int) ==> (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
+theorem "\<And>(y::int) (z::int) n. Suc n < 6 \<Longrightarrow> 3 dvd z \<Longrightarrow>
+    2 dvd (y::int) \<Longrightarrow> (\<exists>(x::int).  2*x = y) \<and> (\<exists>(k::int). 3*k = z)"
   by cooper
 
-theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x "
+theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 \<longrightarrow> y = 5 + x"
   by cooper
 
-lemma "ALL (x::int) >=8. EX i j. 5*i + 3*j = x"
+lemma "\<forall>(x::int) \<ge> 8. \<exists>i j. 5*i + 3*j = x"
   by cooper
 
-lemma "ALL (y::int) (z::int) (n::int). 3 dvd z --> 2 dvd (y::int) --> (EX (x::int).  2*x =  y) & (EX (k::int). 3*k = z)"
+lemma "\<forall>(y::int) (z::int) (n::int).
+    3 dvd z \<longrightarrow> 2 dvd (y::int) \<longrightarrow> (\<exists>(x::int). 2*x = y) \<and> (\<exists>(k::int). 3*k = z)"
   by cooper
 
-lemma "ALL(x::int) y. x < y --> 2 * x + 1 < 2 * y"
+lemma "\<forall>(x::int) y. x < y \<longrightarrow> 2 * x + 1 < 2 * y"
   by cooper
 
-lemma "ALL(x::int) y. 2 * x + 1 ~= 2 * y"
+lemma "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y"
   by cooper
 
-lemma "EX(x::int) y. 0 < x  & 0 <= y  & 3 * x - 5 * y = 1"
+lemma "\<exists>(x::int) y. 0 < x \<and> 0 \<le> y \<and> 3 * x - 5 * y = 1"
   by cooper
 
-lemma "~ (EX(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
+lemma "\<not> (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
   by cooper
 
-lemma "ALL(x::int). (2 dvd x) --> (EX(y::int). x = 2*y)"
+lemma "\<forall>(x::int). 2 dvd x \<longrightarrow> (\<exists>(y::int). x = 2*y)"
   by cooper
 
-lemma "ALL(x::int). (2 dvd x) = (EX(y::int). x = 2*y)"
+lemma "\<forall>(x::int). 2 dvd x \<longleftrightarrow> (\<exists>(y::int). x = 2*y)"
   by cooper
 
-lemma "ALL(x::int). ((2 dvd x) = (ALL(y::int). x ~= 2*y + 1))"
+lemma "\<forall>(x::int). 2 dvd x \<longleftrightarrow> (\<forall>(y::int). x \<noteq> 2*y + 1)"
   by cooper
 
-lemma "~ (ALL(x::int). ((2 dvd x) = (ALL(y::int). x ~= 2*y+1) | (EX(q::int) (u::int) i. 3*i + 2*q - u < 17) --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
-  by cooper
-
-lemma "~ (ALL(i::int). 4 <= i --> (EX x y. 0 <= x & 0 <= y & 3 * x + 5 * y = i))"
+lemma "\<not> (\<forall>(x::int).
+    (2 dvd x \<longleftrightarrow> (ALL(y::int). x \<noteq> 2*y+1) \<or>
+      (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17) \<longrightarrow> 0 < x \<or> (\<not> 3 dvd x \<and> x + 8 = 0)))"
   by cooper
 
-lemma "EX j. ALL (x::int) >= j. EX i j. 5*i + 3*j = x"
+lemma "\<not> (\<forall>(i::int). 4 \<le> i \<longrightarrow> (\<exists>x y. 0 \<le> x \<and> 0 \<le> y \<and> 3 * x + 5 * y = i))"
   by cooper
 
-theorem "(\<forall>(y::int). 3 dvd y) ==> \<forall>(x::int). b < x --> a \<le> x"
+lemma "\<exists>j. \<forall>(x::int) \<ge> j. \<exists>i j. 5*i + 3*j = x"
+  by cooper
+
+theorem "(\<forall>(y::int). 3 dvd y) \<Longrightarrow> \<forall>(x::int). b < x \<longrightarrow> a \<le> x"
   by cooper
 
-theorem "!! (y::int) (z::int) (n::int). 3 dvd z ==> 2 dvd (y::int) ==>
-  (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
+theorem "\<And>(y::int) (z::int) (n::int). 3 dvd z \<Longrightarrow> 2 dvd (y::int) \<Longrightarrow>
+  (\<exists>(x::int). 2*x = y) \<and> (\<exists>(k::int). 3*k = z)"
   by cooper
 
-theorem "!! (y::int) (z::int) n. Suc(n::nat) < 6 ==>  3 dvd z ==>
-  2 dvd (y::int) ==> (\<exists>(x::int).  2*x =  y) & (\<exists>(k::int). 3*k = z)"
+theorem "\<And>(y::int) (z::int) n. Suc n < 6 \<Longrightarrow> 3 dvd z \<Longrightarrow>
+    2 dvd (y::int) \<Longrightarrow> (\<exists>(x::int). 2*x = y) \<and> (\<exists>(k::int). 3*k = z)"
   by cooper
 
-theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 --> y = 5 + x "
+theorem "\<forall>(x::nat). \<exists>(y::nat). (0::nat) \<le> 5 \<longrightarrow> y = 5 + x"
   by cooper
 
-theorem "\<forall>(x::nat). \<exists>(y::nat). y = 5 + x | x div 6 + 1= 2"
+theorem "\<forall>(x::nat). \<exists>(y::nat). y = 5 + x \<or> x div 6 + 1 = 2"
   by cooper
 
 theorem "\<exists>(x::int). 0 < x"
   by cooper
 
-theorem "\<forall>(x::int) y. x < y --> 2 * x + 1 < 2 * y"
+theorem "\<forall>(x::int) y. x < y \<longrightarrow> 2 * x + 1 < 2 * y"
   by cooper
 
 theorem "\<forall>(x::int) y. 2 * x + 1 \<noteq> 2 * y"
@@ -2231,43 +2243,45 @@
 theorem "\<exists>(x::int) y. 0 < x  & 0 \<le> y  & 3 * x - 5 * y = 1"
   by cooper
 
-theorem "~ (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
+theorem "\<not> (\<exists>(x::int) (y::int) (z::int). 4*x + (-6::int)*y = 1)"
   by cooper
 
-theorem "~ (\<exists>(x::int). False)"
+theorem "\<not> (\<exists>(x::int). False)"
   by cooper
 
-theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)"
+theorem "\<forall>(x::int). 2 dvd x \<longrightarrow> (\<exists>(y::int). x = 2*y)"
   by cooper
 
-theorem "\<forall>(x::int). (2 dvd x) --> (\<exists>(y::int). x = 2*y)"
+theorem "\<forall>(x::int). 2 dvd x \<longrightarrow> (\<exists>(y::int). x = 2*y)"
   by cooper
 
-theorem "\<forall>(x::int). (2 dvd x) = (\<exists>(y::int). x = 2*y)"
+theorem "\<forall>(x::int). 2 dvd x \<longleftrightarrow> (\<exists>(y::int). x = 2*y)"
   by cooper
 
-theorem "\<forall>(x::int). ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y + 1))"
+theorem "\<forall>(x::int). 2 dvd x \<longleftrightarrow> (\<forall>(y::int). x \<noteq> 2*y + 1)"
   by cooper
 
-theorem "~ (\<forall>(x::int).
-            ((2 dvd x) = (\<forall>(y::int). x \<noteq> 2*y+1) |
-             (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17)
-             --> 0 < x | ((~ 3 dvd x) &(x + 8 = 0))))"
+theorem
+  "\<not> (\<forall>(x::int).
+    (2 dvd x \<longleftrightarrow>
+      (\<forall>(y::int). x \<noteq> 2*y+1) \<or>
+      (\<exists>(q::int) (u::int) i. 3*i + 2*q - u < 17)
+       \<longrightarrow> 0 < x \<or> (\<not> 3 dvd x \<and> x + 8 = 0)))"
   by cooper
 
-theorem "~ (\<forall>(i::int). 4 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
+theorem "\<not> (\<forall>(i::int). 4 \<le> i \<longrightarrow> (\<exists>x y. 0 \<le> x \<and> 0 \<le> y \<and> 3 * x + 5 * y = i))"
   by cooper
 
-theorem "\<forall>(i::int). 8 \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)"
+theorem "\<forall>(i::int). 8 \<le> i \<longrightarrow> (\<exists>x y. 0 \<le> x \<and> 0 \<le> y \<and> 3 * x + 5 * y = i)"
   by cooper
 
-theorem "\<exists>(j::int). \<forall>i. j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i)"
+theorem "\<exists>(j::int). \<forall>i. j \<le> i \<longrightarrow> (\<exists>x y. 0 \<le> x \<and> 0 \<le> y \<and> 3 * x + 5 * y = i)"
   by cooper
 
-theorem "~ (\<forall>j (i::int). j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
+theorem "\<not> (\<forall>j (i::int). j \<le> i \<longrightarrow> (\<exists>x y. 0 \<le> x \<and> 0 \<le> y \<and> 3 * x + 5 * y = i))"
   by cooper
 
-theorem "(\<exists>m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2"
+theorem "(\<exists>m::nat. n = 2 * m) \<longrightarrow> (n + 1) div 2 = n div 2"
   by cooper
 
 end
diff -r aa1acc25126b -r 557003a7cf78 src/HOL/Decision_Procs/DP_Library.thy
--- a/src/HOL/Decision_Procs/DP_Library.thy	Fri Feb 28 17:54:52 2014 +0100
+++ b/src/HOL/Decision_Procs/DP_Library.thy	Fri Feb 28 22:56:15 2014 +0100
@@ -5,35 +5,36 @@
 primrec alluopairs:: "'a list \<Rightarrow> ('a \<times> 'a) list"
 where
   "alluopairs [] = []"
-| "alluopairs (x#xs) = (map (Pair x) (x#xs))@(alluopairs xs)"
+| "alluopairs (x # xs) = map (Pair x) (x # xs) @ alluopairs xs"
 
-lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x,y). x\<in> set xs \<and> y\<in> set xs}"
+lemma alluopairs_set1: "set (alluopairs xs) \<le> {(x, y). x\<in> set xs \<and> y\<in> set xs}"
   by (induct xs) auto
 
 lemma alluopairs_set:
-  "\<lbrakk>x\<in> set xs ; y \<in> set xs\<rbrakk> \<Longrightarrow> (x,y) \<in> set (alluopairs xs) \<or> (y,x) \<in> set (alluopairs xs) "
+  "x\<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> (x, y) \<in> set (alluopairs xs) \<or> (y, x) \<in> set (alluopairs xs)"
   by (induct xs) auto
 
 lemma alluopairs_bex:
-  assumes Pc: "\<forall> x \<in> set xs. \<forall>y\<in> set xs. P x y = P y x"
-  shows "(\<exists> x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists> (x,y) \<in> set (alluopairs xs). P x y)"
+  assumes Pc: "\<forall>x \<in> set xs. \<forall>y \<in> set xs. P x y = P y x"
+  shows "(\<exists>x \<in> set xs. \<exists>y \<in> set xs. P x y) \<longleftrightarrow> (\<exists>(x, y) \<in> set (alluopairs xs). P x y)"
 proof
-  assume "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y"
-  then obtain x y where x: "x \<in> set xs" and y:"y \<in> set xs" and P: "P x y"
+  assume "\<exists>x \<in> set xs. \<exists>y \<in> set xs. P x y"
+  then obtain x y where x: "x \<in> set xs" and y: "y \<in> set xs" and P: "P x y"
     by blast
-  from alluopairs_set[OF x y] P Pc x y show"\<exists>(x, y)\<in>set (alluopairs xs). P x y" 
+  from alluopairs_set[OF x y] P Pc x y show "\<exists>(x, y) \<in> set (alluopairs xs). P x y" 
     by auto
 next
-  assume "\<exists>(x, y)\<in>set (alluopairs xs). P x y"
-  then obtain "x" and "y" where xy: "(x,y) \<in> set (alluopairs xs)" and P: "P x y"
+  assume "\<exists>(x, y) \<in> set (alluopairs xs). P x y"
+  then obtain x and y where xy: "(x, y) \<in> set (alluopairs xs)" and P: "P x y"
     by blast+
-  from xy have "x \<in> set xs \<and> y\<in> set xs" using alluopairs_set1 by blast
+  from xy have "x \<in> set xs \<and> y \<in> set xs"
+    using alluopairs_set1 by blast
   with P show "\<exists>x\<in>set xs. \<exists>y\<in>set xs. P x y" by blast
 qed
 
 lemma alluopairs_ex:
   "\<forall>x y. P x y = P y x \<Longrightarrow>
-    (\<exists>x \<in> set xs. \<exists> y \<in> set xs. P x y) = (\<exists>(x,y) \<in> set (alluopairs xs). P x y)"
+    (\<exists>x \<in> set xs. \<exists>y \<in> set xs. P x y) = (\<exists>(x, y) \<in> set (alluopairs xs). P x y)"
   by (blast intro!: alluopairs_bex)
 
 end
diff -r aa1acc25126b -r 557003a7cf78 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Fri Feb 28 17:54:52 2014 +0100
+++ b/src/Pure/General/completion.scala	Fri Feb 28 22:56:15 2014 +0100
@@ -188,12 +188,6 @@
 
   /* word parsers */
 
-  def word_context(text: Option[String]): Boolean =
-    text match {
-      case None => false
-      case Some(s) => Word_Parsers.is_word(s)
-    }
-
   private object Word_Parsers extends RegexParsers
   {
     override val whiteSpace = "".r
@@ -206,10 +200,29 @@
     private def word: Parser[String] = word_regex
     private def word3: Parser[String] = """[a-zA-Z0-9_']{3,}""".r
 
-    def is_word(s: CharSequence): Boolean =
-      word_regex.pattern.matcher(s).matches
+    def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
+    def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c)
 
-    def read(explicit: Boolean, in: CharSequence): Option[String] =
+    def extend_word(text: CharSequence, offset: Text.Offset): Text.Offset =
+    {
+      val n = text.length
+      var i = offset
+      while (i < n && is_word_char(text.charAt(i))) i += 1
+      if (i < n && text.charAt(i) == '>' && read_symbol(text.subSequence(0, i + 1)).isDefined)
+        i + 1
+      else i
+    }
+
+    def read_symbol(in: CharSequence): Option[String] =
+    {
+      val reverse_in = new Library.Reverse(in)
+      parse(reverse_symbol ^^ (_.reverse), reverse_in) match {
+        case Success(result, _) => Some(result)
+        case _ => None
+      }
+    }
+
+    def read_word(explicit: Boolean, in: CharSequence): Option[String] =
     {
       val parse_word = if (explicit) word else word3
       val reverse_in = new Library.Reverse(in)
@@ -223,7 +236,7 @@
 
   /* abbreviations */
 
-  private val caret = '\007'
+  private val caret_indicator = '\007'
   private val antiquote = "@{"
   private val default_abbrs =
     Map("@{" -> "@{\007}", "`" -> "\\<open>\007\\<close>")
@@ -278,13 +291,18 @@
     history: Completion.History,
     decode: Boolean,
     explicit: Boolean,
-    text_start: Text.Offset,
+    start: Text.Offset,
     text: CharSequence,
-    word_context: Boolean,
+    caret: Int,
+    extend_word: Boolean,
     language_context: Completion.Language_Context): Option[Completion.Result] =
   {
+    val length = text.length
+
     val abbrevs_result =
-      Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), new Library.Reverse(text)) match {
+    {
+      val reverse_in = new Library.Reverse(text.subSequence(0, caret))
+      Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), reverse_in) match {
         case Scan.Parsers.Success(reverse_a, _) =>
           val abbrevs = abbrevs_map.get_list(reverse_a)
           abbrevs match {
@@ -293,32 +311,42 @@
               val ok =
                 if (a == Completion.antiquote) language_context.antiquotes
                 else language_context.symbols || Completion.default_abbrs.isDefinedAt(a)
-              if (ok) Some((a, abbrevs.map(_._2))) else None
+              if (ok) Some(((a, abbrevs.map(_._2)), caret))
+              else None
           }
         case _ => None
       }
+    }
 
     val words_result =
       abbrevs_result orElse {
-        if (word_context) None
-        else
-          Completion.Word_Parsers.read(explicit, text) match {
-            case Some(word) =>
-              val completions =
-                for {
-                  s <- words_lex.completions(word)
-                  if (if (keywords(s)) language_context.is_outer else language_context.symbols)
-                  r <- words_map.get_list(s)
-                } yield r
-              if (completions.isEmpty) None
-              else Some(word, completions)
-            case None => None
-          }
+        val end =
+          if (extend_word) Completion.Word_Parsers.extend_word(text, caret)
+          else caret
+        (Completion.Word_Parsers.read_symbol(text.subSequence(0, end)) match {
+          case Some(symbol) => Some(symbol)
+          case None =>
+            val word_context =
+              end < length && Completion.Word_Parsers.is_word_char(text.charAt(end))
+            if (word_context) None
+            else Completion.Word_Parsers.read_word(explicit, text.subSequence(0, end))
+        }) match {
+          case Some(word) =>
+            val completions =
+              for {
+                s <- words_lex.completions(word)
+                if (if (keywords(s)) language_context.is_outer else language_context.symbols)
+                r <- words_map.get_list(s)
+              } yield r
+            if (completions.isEmpty) None
+            else Some(((word, completions), end))
+          case None => None
+        }
       }
 
     words_result match {
-      case Some((word, cs)) =>
-        val range = Text.Range(- word.length, 0) + (text_start + text.length)
+      case Some(((word, cs), end)) =>
+        val range = Text.Range(- word.length, 0) + end + start
         val ds = (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word)
         if (ds.isEmpty) None
         else {
@@ -328,7 +356,7 @@
           val items =
             ds.map(s => {
               val (s1, s2) =
-                space_explode(Completion.caret, s) match {
+                space_explode(Completion.caret_indicator, s) match {
                   case List(s1, s2) => (s1, s2)
                   case _ => (s, "")
                 }
diff -r aa1acc25126b -r 557003a7cf78 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Fri Feb 28 17:54:52 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Feb 28 22:56:15 2014 +0100
@@ -141,13 +141,11 @@
       Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
         case Some(syntax) =>
           val caret = text_area.getCaretPosition
+
           val line = buffer.getLineOfOffset(caret)
-          val start = buffer.getLineStartOffset(line)
-          val text = buffer.getSegment(start, caret - start)
-
-          val word_context =
-            Completion.word_context(
-              JEdit_Lib.try_get_text(buffer, JEdit_Lib.point_range(buffer, caret)))
+          val line_start = buffer.getLineStartOffset(line)
+          val line_length = (buffer.getLineEndOffset(line) min buffer.getLength) - line_start
+          val line_text = buffer.getSegment(line_start, line_length)
 
           val context =
             (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
@@ -156,7 +154,8 @@
               case None => None
             }) getOrElse syntax.language_context
 
-          syntax.completion.complete(history, decode, explicit, start, text, word_context, context)
+          syntax.completion.complete(
+            history, decode, explicit, line_start, line_text, caret - line_start, true, context)
 
         case None => None
       }
@@ -387,15 +386,11 @@
           val history = PIDE.completion_history.value
 
           val caret = text_field.getCaret.getDot
-          val text = text_field.getText.substring(0, caret)
-
-          val word_context =
-            Completion.word_context(JEdit_Lib.try_get_text(text_field.getText,
-              Text.Range(caret, caret + 1)))  // FIXME proper point range!?
+          val text = text_field.getText
 
           val context = syntax.language_context
 
-          syntax.completion.complete(history, true, false, 0, text, word_context, context) match {
+          syntax.completion.complete(history, true, false, 0, text, caret, false, context) match {
             case Some(result) =>
               val fm = text_field.getFontMetrics(text_field.getFont)
               val loc =
diff -r aa1acc25126b -r 557003a7cf78 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Feb 28 17:54:52 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Feb 28 22:56:15 2014 +0100
@@ -155,12 +155,6 @@
     catch { case _: IndexOutOfBoundsException => None }
 
 
-  /* buffer range */
-
-  def buffer_range(buffer: JEditBuffer): Text.Range =
-    Text.Range(0, (buffer.getLength - 1) max 0)
-
-
   /* point range */
 
   def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
@@ -179,7 +173,10 @@
     }
 
 
-  /* visible text range */
+  /* text ranges */
+
+  def buffer_range(buffer: JEditBuffer): Text.Range =
+    Text.Range(0, buffer.getLength)
 
   def visible_range(text_area: TextArea): Option[Text.Range] =
   {
@@ -197,9 +194,13 @@
   def invalidate_range(text_area: TextArea, range: Text.Range)
   {
     val buffer = text_area.getBuffer
-    text_area.invalidateLineRange(
-      buffer.getLineOfOffset(range.start),
-      buffer.getLineOfOffset(range.stop))
+    buffer_range(buffer).try_restrict(range) match {
+      case Some(range1) if !range1.is_singularity =>
+        text_area.invalidateLineRange(
+          buffer.getLineOfOffset(range1.start),
+          buffer.getLineOfOffset(range1.stop))
+      case _ =>
+    }
   }