allow short words for explicit completion;

--- a/src/Pure/Isar/completion.scala	Fri Aug 30 12:33:16 2013 +0200
+++ b/src/Pure/Isar/completion.scala	Fri Aug 30 12:44:39 2013 +0200
@@ -39,12 +39,14 @@
     def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
     def reverse_symb: 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 word: Parser[String] = word_regex
+    def word3: Parser[String] = """[a-zA-Z0-9_']{3,}""".r
 
-    def read(in: CharSequence): Option[String] =
+    def read(explicit: Boolean, in: CharSequence): Option[String] =
     {
+      val parse_word = if (explicit) word else word3
       val reverse_in = new Library.Reverse(in)
-      parse((reverse_symbol | reverse_symb | escape | word) ^^ (_.reverse), reverse_in) match {
+      parse((reverse_symbol | reverse_symb | escape | parse_word) ^^ (_.reverse), reverse_in) match {
         case Success(result, _) => Some(result)
         case _ => None
       }
@@ -90,7 +92,8 @@
 
   /* complete */
 
-  def complete(decode: Boolean, line: CharSequence): Option[(String, List[Completion.Item])] =
+  def complete(decode: Boolean, explicit: Boolean, line: CharSequence)
+    : Option[(String, List[Completion.Item])] =
   {
     val raw_result =
       abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
@@ -101,7 +104,7 @@
             case (a, _) :: _ => Some((a, abbrevs.map(_._2)))
           }
         case _ =>
-          Completion.Parse.read(line) match {
+          Completion.Parse.read(explicit, line) match {
             case Some(word) =>
               words_lex.completions(word).map(words_map.get_list(_)).flatten match {
                 case Nil => None

--- a/src/Tools/jEdit/src/completion_popup.scala	Fri Aug 30 12:33:16 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Aug 30 12:44:39 2013 +0200
@@ -91,7 +91,7 @@
       }
     }
 
-    def action(immediate: Boolean)
+    def action(immediate: Boolean = false, explicit: Boolean = false)
     {
       val view = text_area.getView
       val layered = view.getLayeredPane
@@ -106,7 +106,8 @@
             val start = buffer.getLineStartOffset(line)
             val text = buffer.getSegment(start, caret - start)
 
-            syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match {
+            val decode = Isabelle_Encoding.is_active(buffer)
+            syntax.completion.complete(decode, explicit, text) match {
               case Some((_, List(item))) if item.immediate && immediate =>
                 insert(item)
 
@@ -161,7 +162,7 @@
 
           if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
             input_delay.revoke()
-            action(PIDE.options.bool("jedit_completion_immediate"))
+            action(immediate = PIDE.options.bool("jedit_completion_immediate"))
           }
           else input_delay.invoke()
         }
@@ -170,7 +171,7 @@
 
     private val input_delay =
       Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
-        action(false)
+        action()
       }
 
 

--- a/src/Tools/jEdit/src/isabelle.scala	Fri Aug 30 12:33:16 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Aug 30 12:44:39 2013 +0200
@@ -168,7 +168,8 @@
   def complete(view: View)
   {
     Completion_Popup.Text_Area(view.getTextArea) match {
-      case Some(text_area_completion) => text_area_completion.action(true)
+      case Some(text_area_completion) =>
+        text_area_completion.action(immediate = true, explicit = true)
       case None => CompleteWord.completeWord(view)
     }
   }