discontinued unfinished attempts at syntactic word context (see 2e1398b484aa, 08a1c860bc12, 7f229b0212fe) -- back to more basic completion of Isabelle2013-2;
authorwenzelm
Mon Jul 21 13:50:26 2014 +0200 (2014-07-21)
changeset 57588ff31aad27661
parent 57587 af074bd6222e
child 57589 e0e4ac981cf1
discontinued unfinished attempts at syntactic word context (see 2e1398b484aa, 08a1c860bc12, 7f229b0212fe) -- back to more basic completion of Isabelle2013-2;
src/Pure/General/completion.scala
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Pure/General/completion.scala	Mon Jul 21 12:25:54 2014 +0200
     1.2 +++ b/src/Pure/General/completion.scala	Mon Jul 21 13:50:26 2014 +0200
     1.3 @@ -231,16 +231,6 @@
     1.4      def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
     1.5      def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.'
     1.6  
     1.7 -    def extend_word(text: CharSequence, offset: Text.Offset): Text.Offset =
     1.8 -    {
     1.9 -      val n = text.length
    1.10 -      var i = offset
    1.11 -      while (i < n && is_word_char(text.charAt(i))) i += 1
    1.12 -      if (i < n && text.charAt(i) == '>' && read_symbol(text.subSequence(0, i + 1)).isDefined)
    1.13 -        i + 1
    1.14 -      else i
    1.15 -    }
    1.16 -
    1.17      def read_symbol(in: CharSequence): Option[String] =
    1.18      {
    1.19        val reverse_in = new Library.Reverse(in)
    1.20 @@ -341,7 +331,6 @@
    1.21      start: Text.Offset,
    1.22      text: CharSequence,
    1.23      caret: Int,
    1.24 -    extend_word: Boolean,
    1.25      language_context: Completion.Language_Context): Option[Completion.Result] =
    1.26    {
    1.27      def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
    1.28 @@ -359,7 +348,7 @@
    1.29                val ok =
    1.30                  if (a == Completion.antiquote) language_context.antiquotes
    1.31                  else language_context.symbols || Completion.default_abbrs.exists(_._1 == a)
    1.32 -              if (ok) Some(((a, abbrevs), caret))
    1.33 +              if (ok) Some((a, abbrevs))
    1.34                else None
    1.35            }
    1.36          case _ => None
    1.37 @@ -369,17 +358,10 @@
    1.38      val words_result =
    1.39        if (abbrevs_result.isDefined) None
    1.40        else {
    1.41 -        val end =
    1.42 -          if (extend_word) Completion.Word_Parsers.extend_word(text, caret)
    1.43 -          else caret
    1.44          val result =
    1.45 -          Completion.Word_Parsers.read_symbol(text.subSequence(0, end)) match {
    1.46 +          Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) match {
    1.47              case Some(symbol) => Some((symbol, ""))
    1.48 -            case None =>
    1.49 -              val word_context =
    1.50 -                end < length && Completion.Word_Parsers.is_word_char(text.charAt(end))
    1.51 -              if (word_context) None
    1.52 -              else Completion.Word_Parsers.read_word(explicit, text.subSequence(0, end))
    1.53 +            case None => Completion.Word_Parsers.read_word(explicit, text.subSequence(0, caret))
    1.54            }
    1.55          result.map(
    1.56            {
    1.57 @@ -397,13 +379,13 @@
    1.58                      if ok
    1.59                      completion <- words_map.get_list(complete_word)
    1.60                    } yield (complete_word, completion)
    1.61 -              (((full_word, completions), end))
    1.62 +              ((full_word, completions))
    1.63            })
    1.64        }
    1.65  
    1.66      (abbrevs_result orElse words_result) match {
    1.67 -      case Some(((original, completions), end)) if !completions.isEmpty =>
    1.68 -        val range = Text.Range(- original.length, 0) + end + start
    1.69 +      case Some((original, completions)) if !completions.isEmpty =>
    1.70 +        val range = Text.Range(- original.length, 0) + caret + start
    1.71          val immediate =
    1.72            explicit ||
    1.73              (!Completion.Word_Parsers.is_word(original) &&
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Mon Jul 21 12:25:54 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Jul 21 13:50:26 2014 +0200
     2.3 @@ -171,7 +171,7 @@
     2.4              line_text <- JEdit_Lib.try_get_text(buffer, line_range)
     2.5              result <-
     2.6                syntax.completion.complete(
     2.7 -                history, decode, explicit, line_start, line_text, caret - line_start, false, context)
     2.8 +                history, decode, explicit, line_start, line_text, caret - line_start, context)
     2.9            } yield result
    2.10  
    2.11          case None => None
    2.12 @@ -558,7 +558,7 @@
    2.13  
    2.14            val context = syntax.language_context
    2.15  
    2.16 -          syntax.completion.complete(history, true, false, 0, text, caret, false, context) match {
    2.17 +          syntax.completion.complete(history, true, false, 0, text, caret, context) match {
    2.18              case Some(result) =>
    2.19                val fm = text_field.getFontMetrics(text_field.getFont)
    2.20                val loc =