allow short words for explicit completion;
authorwenzelm
Fri Aug 30 12:44:39 2013 +0200 (2013-08-30)
changeset 53322a4cd032172e0
parent 53321 53c314f1e8bf
child 53323 5fa77d6ad63d
allow short words for explicit completion;
src/Pure/Isar/completion.scala
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/isabelle.scala
     1.1 --- a/src/Pure/Isar/completion.scala	Fri Aug 30 12:33:16 2013 +0200
     1.2 +++ b/src/Pure/Isar/completion.scala	Fri Aug 30 12:44:39 2013 +0200
     1.3 @@ -39,12 +39,14 @@
     1.4      def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
     1.5      def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
     1.6      def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
     1.7 -    def word: Parser[String] = """[a-zA-Z0-9_']{3,}""".r
     1.8 +    def word: Parser[String] = word_regex
     1.9 +    def word3: Parser[String] = """[a-zA-Z0-9_']{3,}""".r
    1.10  
    1.11 -    def read(in: CharSequence): Option[String] =
    1.12 +    def read(explicit: Boolean, in: CharSequence): Option[String] =
    1.13      {
    1.14 +      val parse_word = if (explicit) word else word3
    1.15        val reverse_in = new Library.Reverse(in)
    1.16 -      parse((reverse_symbol | reverse_symb | escape | word) ^^ (_.reverse), reverse_in) match {
    1.17 +      parse((reverse_symbol | reverse_symb | escape | parse_word) ^^ (_.reverse), reverse_in) match {
    1.18          case Success(result, _) => Some(result)
    1.19          case _ => None
    1.20        }
    1.21 @@ -90,7 +92,8 @@
    1.22  
    1.23    /* complete */
    1.24  
    1.25 -  def complete(decode: Boolean, line: CharSequence): Option[(String, List[Completion.Item])] =
    1.26 +  def complete(decode: Boolean, explicit: Boolean, line: CharSequence)
    1.27 +    : Option[(String, List[Completion.Item])] =
    1.28    {
    1.29      val raw_result =
    1.30        abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
    1.31 @@ -101,7 +104,7 @@
    1.32              case (a, _) :: _ => Some((a, abbrevs.map(_._2)))
    1.33            }
    1.34          case _ =>
    1.35 -          Completion.Parse.read(line) match {
    1.36 +          Completion.Parse.read(explicit, line) match {
    1.37              case Some(word) =>
    1.38                words_lex.completions(word).map(words_map.get_list(_)).flatten match {
    1.39                  case Nil => None
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Fri Aug 30 12:33:16 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Aug 30 12:44:39 2013 +0200
     2.3 @@ -91,7 +91,7 @@
     2.4        }
     2.5      }
     2.6  
     2.7 -    def action(immediate: Boolean)
     2.8 +    def action(immediate: Boolean = false, explicit: Boolean = false)
     2.9      {
    2.10        val view = text_area.getView
    2.11        val layered = view.getLayeredPane
    2.12 @@ -106,7 +106,8 @@
    2.13              val start = buffer.getLineStartOffset(line)
    2.14              val text = buffer.getSegment(start, caret - start)
    2.15  
    2.16 -            syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match {
    2.17 +            val decode = Isabelle_Encoding.is_active(buffer)
    2.18 +            syntax.completion.complete(decode, explicit, text) match {
    2.19                case Some((_, List(item))) if item.immediate && immediate =>
    2.20                  insert(item)
    2.21  
    2.22 @@ -161,7 +162,7 @@
    2.23  
    2.24            if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
    2.25              input_delay.revoke()
    2.26 -            action(PIDE.options.bool("jedit_completion_immediate"))
    2.27 +            action(immediate = PIDE.options.bool("jedit_completion_immediate"))
    2.28            }
    2.29            else input_delay.invoke()
    2.30          }
    2.31 @@ -170,7 +171,7 @@
    2.32  
    2.33      private val input_delay =
    2.34        Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
    2.35 -        action(false)
    2.36 +        action()
    2.37        }
    2.38  
    2.39  
     3.1 --- a/src/Tools/jEdit/src/isabelle.scala	Fri Aug 30 12:33:16 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Fri Aug 30 12:44:39 2013 +0200
     3.3 @@ -168,7 +168,8 @@
     3.4    def complete(view: View)
     3.5    {
     3.6      Completion_Popup.Text_Area(view.getTextArea) match {
     3.7 -      case Some(text_area_completion) => text_area_completion.action(true)
     3.8 +      case Some(text_area_completion) =>
     3.9 +        text_area_completion.action(immediate = true, explicit = true)
    3.10        case None => CompleteWord.completeWord(view)
    3.11      }
    3.12    }