src/Pure/General/completion.scala
changeset 63887 2d9c12eba726
parent 63873 228a85f1d6af
child 65344 b99283eed13c
equal deleted inserted replaced
63885:a6cd18af8bf9 63887:2d9c12eba726
   262     private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
   262     private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
   263     private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
   263     private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
   264     private def reverse_escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
   264     private def reverse_escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
   265 
   265 
   266     private val word_regex = "[a-zA-Z0-9_'.]+".r
   266     private val word_regex = "[a-zA-Z0-9_'.]+".r
   267     private def word: Parser[String] = word_regex
   267     private def word2: Parser[String] = "[a-zA-Z0-9_'.]{2,}".r
   268     private def word3: Parser[String] = "[a-zA-Z0-9_'.]{3,}".r
       
   269     private def underscores: Parser[String] = "_*".r
   268     private def underscores: Parser[String] = "_*".r
   270 
   269 
   271     def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
   270     def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
   272     def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.'
   271     def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.'
   273 
   272 
   278         case Success(result, _) => Some(result)
   277         case Success(result, _) => Some(result)
   279         case _ => None
   278         case _ => None
   280       }
   279       }
   281     }
   280     }
   282 
   281 
   283     def read_word(explicit: Boolean, in: CharSequence): Option[(String, String)] =
   282     def read_word(in: CharSequence): Option[(String, String)] =
   284     {
   283     {
   285       val parse_word = if (explicit) word else word3
       
   286       val reverse_in = new Library.Reverse(in)
   284       val reverse_in = new Library.Reverse(in)
   287       val parser =
   285       val parser =
   288         (reverse_symbol | reverse_symb | reverse_escape) ^^ (x => (x.reverse, "")) |
   286         (reverse_symbol | reverse_symb | reverse_escape) ^^ (x => (x.reverse, "")) |
   289         underscores ~ parse_word ~ opt("?") ^^
   287         underscores ~ word2 ~ opt("?") ^^
   290         { case x ~ y ~ z => (z.getOrElse("") + y.reverse, x) }
   288         { case x ~ y ~ z => (z.getOrElse("") + y.reverse, x) }
   291       parse(parser, reverse_in) match {
   289       parse(parser, reverse_in) match {
   292         case Success(result, _) => Some(result)
   290         case Success(result, _) => Some(result)
   293         case _ => None
   291         case _ => None
   294       }
   292       }
   446         val word_context =
   444         val word_context =
   447           caret < length && Completion.Word_Parsers.is_word_char(text.charAt(caret))
   445           caret < length && Completion.Word_Parsers.is_word_char(text.charAt(caret))
   448         val result =
   446         val result =
   449           Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) match {
   447           Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) match {
   450             case Some(symbol) => Some((symbol, ""))
   448             case Some(symbol) => Some((symbol, ""))
   451             case None => Completion.Word_Parsers.read_word(explicit, text.subSequence(0, caret))
   449             case None => Completion.Word_Parsers.read_word(text.subSequence(0, caret))
   452           }
   450           }
   453         result.map(
   451         result.map(
   454           {
   452           {
   455             case (word, underscores) =>
   453             case (word, underscores) =>
   456               val complete_words = words_lex.completions(word)
   454               val complete_words = words_lex.completions(word)