--- 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
--- 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
--- 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, "")
}
--- 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 =
--- 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 _ =>
+ }
}