complete symbols only in backslash forms -- less intrusive editing, greater chance of finding escape sequence in text;
complete words >= 3 characters only;
discontinued short word abbrev "Un" (see also fdd6e68e29d9 and e38e80686ce5);
--- a/NEWS Wed Aug 28 19:12:15 2013 +0200
+++ b/NEWS Wed Aug 28 22:25:14 2013 +0200
@@ -90,6 +90,11 @@
according to Isabelle/Scala plugin option "jedit_font_reset_size"
(cf. keyboard shortcut C+0).
+* More reactive and less intrusive completion. Plain words need to be
+at least 3 characters long to be completed (was 2 before). Symbols
+are only completed in backslash forms, e.g. \forall or \<forall> that
+both produce the Isabelle symbol \<forall> in its Unicode rendering.
+
*** Pure ***
--- a/etc/symbols Wed Aug 28 19:12:15 2013 +0200
+++ b/etc/symbols Wed Aug 28 22:25:14 2013 +0200
@@ -240,10 +240,10 @@
\<sqsupset> code: 0x002290 group: relation
\<sqsubseteq> code: 0x002291 group: relation abbrev: [=
\<sqsupseteq> code: 0x002292 group: relation abbrev: =]
-\<inter> code: 0x002229 group: operator abbrev: Int
-\<Inter> code: 0x0022c2 group: operator abbrev: Inter
-\<union> code: 0x00222a group: operator abbrev: Un
-\<Union> code: 0x0022c3 group: operator abbrev: Union
+\<inter> code: 0x002229 group: operator
+\<Inter> code: 0x0022c2 group: operator
+\<union> code: 0x00222a group: operator
+\<Union> code: 0x0022c3 group: operator
\<squnion> code: 0x002294 group: operator
\<Squnion> code: 0x002a06 group: operator
\<sqinter> code: 0x002293 group: operator
--- a/src/Pure/Thy/completion.scala Wed Aug 28 19:12:15 2013 +0200
+++ b/src/Pure/Thy/completion.scala Wed Aug 28 22:25:14 2013 +0200
@@ -27,12 +27,13 @@
def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
- def word: Parser[String] = "[a-zA-Z0-9_']{2,}".r
+ def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
+ def word: Parser[String] = """[a-zA-Z0-9_']{3,}""".r
def read(in: CharSequence): Option[String] =
{
val reverse_in = new Library.Reverse(in)
- parse((reverse_symbol | reverse_symb | word) ^^ (_.reverse), reverse_in) match {
+ parse((reverse_symbol | reverse_symb | escape | word) ^^ (_.reverse), reverse_in) match {
case Success(result, _) => Some(result)
case _ => None
}
@@ -61,7 +62,7 @@
{
val words =
(for ((x, _) <- Symbol.names) yield (x, x)).toList :::
- (for ((x, y) <- Symbol.names) yield (y, x)).toList :::
+ (for ((x, y) <- Symbol.names) yield ("\\" + y, x)).toList :::
(for ((x, y) <- Symbol.abbrevs if Completion.is_word(y)) yield (y, x)).toList
val abbrs =