# HG changeset patch
# User wenzelm
# Date 1377721514 -7200
# Node ID 7facc08da8060f81f4736f710d07f9489de58c05
# Parent  31f956f42e8d0d6ccb16f290e4edf90c9c5e01b3
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);

diff -r 31f956f42e8d -r 7facc08da806 NEWS
--- 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 ***
 
diff -r 31f956f42e8d -r 7facc08da806 etc/symbols
--- 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
diff -r 31f956f42e8d -r 7facc08da806 src/Pure/Thy/completion.scala
--- 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 =