# HG changeset patch
# User wenzelm
# Date 1405943426 -7200
# Node ID ff31aad27661f4c8a15b5be9e555c5d6e158b0fa
# Parent  af074bd6222e57bf32bea08cf211967a9982b5ca
discontinued unfinished attempts at syntactic word context (see 2e1398b484aa, 08a1c860bc12, 7f229b0212fe) -- back to more basic completion of Isabelle2013-2;

diff -r af074bd6222e -r ff31aad27661 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Mon Jul 21 12:25:54 2014 +0200
+++ b/src/Pure/General/completion.scala	Mon Jul 21 13:50:26 2014 +0200
@@ -231,16 +231,6 @@
     def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
     def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.'
 
-    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)
@@ -341,7 +331,6 @@
     start: Text.Offset,
     text: CharSequence,
     caret: Int,
-    extend_word: Boolean,
     language_context: Completion.Language_Context): Option[Completion.Result] =
   {
     def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
@@ -359,7 +348,7 @@
               val ok =
                 if (a == Completion.antiquote) language_context.antiquotes
                 else language_context.symbols || Completion.default_abbrs.exists(_._1 == a)
-              if (ok) Some(((a, abbrevs), caret))
+              if (ok) Some((a, abbrevs))
               else None
           }
         case _ => None
@@ -369,17 +358,10 @@
     val words_result =
       if (abbrevs_result.isDefined) None
       else {
-        val end =
-          if (extend_word) Completion.Word_Parsers.extend_word(text, caret)
-          else caret
         val result =
-          Completion.Word_Parsers.read_symbol(text.subSequence(0, end)) match {
+          Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) 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))
+            case None => Completion.Word_Parsers.read_word(explicit, text.subSequence(0, caret))
           }
         result.map(
           {
@@ -397,13 +379,13 @@
                     if ok
                     completion <- words_map.get_list(complete_word)
                   } yield (complete_word, completion)
-              (((full_word, completions), end))
+              ((full_word, completions))
           })
       }
 
     (abbrevs_result orElse words_result) match {
-      case Some(((original, completions), end)) if !completions.isEmpty =>
-        val range = Text.Range(- original.length, 0) + end + start
+      case Some((original, completions)) if !completions.isEmpty =>
+        val range = Text.Range(- original.length, 0) + caret + start
         val immediate =
           explicit ||
             (!Completion.Word_Parsers.is_word(original) &&
diff -r af074bd6222e -r ff31aad27661 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Mon Jul 21 12:25:54 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Jul 21 13:50:26 2014 +0200
@@ -171,7 +171,7 @@
             line_text <- JEdit_Lib.try_get_text(buffer, line_range)
             result <-
               syntax.completion.complete(
-                history, decode, explicit, line_start, line_text, caret - line_start, false, context)
+                history, decode, explicit, line_start, line_text, caret - line_start, context)
           } yield result
 
         case None => None
@@ -558,7 +558,7 @@
 
           val context = syntax.language_context
 
-          syntax.completion.complete(history, true, false, 0, text, caret, false, context) match {
+          syntax.completion.complete(history, true, false, 0, text, caret, context) match {
             case Some(result) =>
               val fm = text_field.getFontMetrics(text_field.getFont)
               val loc =