allow completion within a word (or symbol), like semantic completion;
authorwenzelm
Fri Feb 28 22:19:29 2014 +0100 (2014-02-28 ago)
changeset 5581308a1c860bc12
parent 55812 59fcd209cc0c
child 55814 aefa1db74d9d
allow completion within a word (or symbol), like semantic completion;
no special treatment for History_Text_Field, due to lack of active range rendering;
src/Pure/General/completion.scala
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Pure/General/completion.scala	Fri Feb 28 22:11:52 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Fri Feb 28 22:19:29 2014 +0100
     1.3 @@ -188,12 +188,6 @@
     1.4  
     1.5    /* word parsers */
     1.6  
     1.7 -  def word_context(text: Option[String]): Boolean =
     1.8 -    text match {
     1.9 -      case None => false
    1.10 -      case Some(s) => Word_Parsers.is_word(s)
    1.11 -    }
    1.12 -
    1.13    private object Word_Parsers extends RegexParsers
    1.14    {
    1.15      override val whiteSpace = "".r
    1.16 @@ -206,10 +200,29 @@
    1.17      private def word: Parser[String] = word_regex
    1.18      private def word3: Parser[String] = """[a-zA-Z0-9_']{3,}""".r
    1.19  
    1.20 -    def is_word(s: CharSequence): Boolean =
    1.21 -      word_regex.pattern.matcher(s).matches
    1.22 +    def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
    1.23 +    def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c)
    1.24  
    1.25 -    def read(explicit: Boolean, in: CharSequence): Option[String] =
    1.26 +    def extend_word(text: CharSequence, offset: Text.Offset): Text.Offset =
    1.27 +    {
    1.28 +      val n = text.length
    1.29 +      var i = offset
    1.30 +      while (i < n && is_word_char(text.charAt(i))) i += 1
    1.31 +      if (i < n && text.charAt(i) == '>' && read_symbol(text.subSequence(0, i + 1)).isDefined)
    1.32 +        i + 1
    1.33 +      else i
    1.34 +    }
    1.35 +
    1.36 +    def read_symbol(in: CharSequence): Option[String] =
    1.37 +    {
    1.38 +      val reverse_in = new Library.Reverse(in)
    1.39 +      parse(reverse_symbol ^^ (_.reverse), reverse_in) match {
    1.40 +        case Success(result, _) => Some(result)
    1.41 +        case _ => None
    1.42 +      }
    1.43 +    }
    1.44 +
    1.45 +    def read_word(explicit: Boolean, in: CharSequence): Option[String] =
    1.46      {
    1.47        val parse_word = if (explicit) word else word3
    1.48        val reverse_in = new Library.Reverse(in)
    1.49 @@ -223,7 +236,7 @@
    1.50  
    1.51    /* abbreviations */
    1.52  
    1.53 -  private val caret = '\007'
    1.54 +  private val caret_indicator = '\007'
    1.55    private val antiquote = "@{"
    1.56    private val default_abbrs =
    1.57      Map("@{" -> "@{\007}", "`" -> "\\<open>\007\\<close>")
    1.58 @@ -278,13 +291,18 @@
    1.59      history: Completion.History,
    1.60      decode: Boolean,
    1.61      explicit: Boolean,
    1.62 -    text_start: Text.Offset,
    1.63 +    start: Text.Offset,
    1.64      text: CharSequence,
    1.65 -    word_context: Boolean,
    1.66 +    caret: Int,
    1.67 +    extend_word: Boolean,
    1.68      language_context: Completion.Language_Context): Option[Completion.Result] =
    1.69    {
    1.70 +    val length = text.length
    1.71 +
    1.72      val abbrevs_result =
    1.73 -      Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), new Library.Reverse(text)) match {
    1.74 +    {
    1.75 +      val reverse_in = new Library.Reverse(text.subSequence(0, caret))
    1.76 +      Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), reverse_in) match {
    1.77          case Scan.Parsers.Success(reverse_a, _) =>
    1.78            val abbrevs = abbrevs_map.get_list(reverse_a)
    1.79            abbrevs match {
    1.80 @@ -293,32 +311,42 @@
    1.81                val ok =
    1.82                  if (a == Completion.antiquote) language_context.antiquotes
    1.83                  else language_context.symbols || Completion.default_abbrs.isDefinedAt(a)
    1.84 -              if (ok) Some((a, abbrevs.map(_._2))) else None
    1.85 +              if (ok) Some(((a, abbrevs.map(_._2)), caret))
    1.86 +              else None
    1.87            }
    1.88          case _ => None
    1.89        }
    1.90 +    }
    1.91  
    1.92      val words_result =
    1.93        abbrevs_result orElse {
    1.94 -        if (word_context) None
    1.95 -        else
    1.96 -          Completion.Word_Parsers.read(explicit, text) match {
    1.97 -            case Some(word) =>
    1.98 -              val completions =
    1.99 -                for {
   1.100 -                  s <- words_lex.completions(word)
   1.101 -                  if (if (keywords(s)) language_context.is_outer else language_context.symbols)
   1.102 -                  r <- words_map.get_list(s)
   1.103 -                } yield r
   1.104 -              if (completions.isEmpty) None
   1.105 -              else Some(word, completions)
   1.106 -            case None => None
   1.107 -          }
   1.108 +        val end =
   1.109 +          if (extend_word) Completion.Word_Parsers.extend_word(text, caret)
   1.110 +          else caret
   1.111 +        (Completion.Word_Parsers.read_symbol(text.subSequence(0, end)) match {
   1.112 +          case Some(symbol) => Some(symbol)
   1.113 +          case None =>
   1.114 +            val word_context =
   1.115 +              end < length && Completion.Word_Parsers.is_word_char(text.charAt(end))
   1.116 +            if (word_context) None
   1.117 +            else Completion.Word_Parsers.read_word(explicit, text.subSequence(0, end))
   1.118 +        }) match {
   1.119 +          case Some(word) =>
   1.120 +            val completions =
   1.121 +              for {
   1.122 +                s <- words_lex.completions(word)
   1.123 +                if (if (keywords(s)) language_context.is_outer else language_context.symbols)
   1.124 +                r <- words_map.get_list(s)
   1.125 +              } yield r
   1.126 +            if (completions.isEmpty) None
   1.127 +            else Some(((word, completions), end))
   1.128 +          case None => None
   1.129 +        }
   1.130        }
   1.131  
   1.132      words_result match {
   1.133 -      case Some((word, cs)) =>
   1.134 -        val range = Text.Range(- word.length, 0) + (text_start + text.length)
   1.135 +      case Some(((word, cs), end)) =>
   1.136 +        val range = Text.Range(- word.length, 0) + end + start
   1.137          val ds = (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word)
   1.138          if (ds.isEmpty) None
   1.139          else {
   1.140 @@ -328,7 +356,7 @@
   1.141            val items =
   1.142              ds.map(s => {
   1.143                val (s1, s2) =
   1.144 -                space_explode(Completion.caret, s) match {
   1.145 +                space_explode(Completion.caret_indicator, s) match {
   1.146                    case List(s1, s2) => (s1, s2)
   1.147                    case _ => (s, "")
   1.148                  }
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Fri Feb 28 22:11:52 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Feb 28 22:19:29 2014 +0100
     2.3 @@ -141,13 +141,11 @@
     2.4        Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
     2.5          case Some(syntax) =>
     2.6            val caret = text_area.getCaretPosition
     2.7 +
     2.8            val line = buffer.getLineOfOffset(caret)
     2.9 -          val start = buffer.getLineStartOffset(line)
    2.10 -          val text = buffer.getSegment(start, caret - start)
    2.11 -
    2.12 -          val word_context =
    2.13 -            Completion.word_context(
    2.14 -              JEdit_Lib.try_get_text(buffer, JEdit_Lib.point_range(buffer, caret)))
    2.15 +          val line_start = buffer.getLineStartOffset(line)
    2.16 +          val line_length = (buffer.getLineEndOffset(line) min buffer.getLength) - line_start
    2.17 +          val line_text = buffer.getSegment(line_start, line_length)
    2.18  
    2.19            val context =
    2.20              (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
    2.21 @@ -156,7 +154,8 @@
    2.22                case None => None
    2.23              }) getOrElse syntax.language_context
    2.24  
    2.25 -          syntax.completion.complete(history, decode, explicit, start, text, word_context, context)
    2.26 +          syntax.completion.complete(
    2.27 +            history, decode, explicit, line_start, line_text, caret - line_start, true, context)
    2.28  
    2.29          case None => None
    2.30        }
    2.31 @@ -387,15 +386,11 @@
    2.32            val history = PIDE.completion_history.value
    2.33  
    2.34            val caret = text_field.getCaret.getDot
    2.35 -          val text = text_field.getText.substring(0, caret)
    2.36 -
    2.37 -          val word_context =
    2.38 -            Completion.word_context(JEdit_Lib.try_get_text(text_field.getText,
    2.39 -              Text.Range(caret, caret + 1)))  // FIXME proper point range!?
    2.40 +          val text = text_field.getText
    2.41  
    2.42            val context = syntax.language_context
    2.43  
    2.44 -          syntax.completion.complete(history, true, false, 0, text, word_context, context) match {
    2.45 +          syntax.completion.complete(history, true, false, 0, text, caret, false, context) match {
    2.46              case Some(result) =>
    2.47                val fm = text_field.getFontMetrics(text_field.getFont)
    2.48                val loc =