# HG changeset patch
# User wenzelm
# Date 1393622369 -3600
# Node ID 08a1c860bc122f3b4677163df93d20af92ab54a8
# Parent  59fcd209cc0cd5c056b43a1c370c98465f696dce
allow completion within a word (or symbol), like semantic completion;
no special treatment for History_Text_Field, due to lack of active range rendering;

diff -r 59fcd209cc0c -r 08a1c860bc12 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Fri Feb 28 22:11:52 2014 +0100
+++ b/src/Pure/General/completion.scala	Fri Feb 28 22:19:29 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 59fcd209cc0c -r 08a1c860bc12 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Fri Feb 28 22:11:52 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Feb 28 22:19:29 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 =