src/Pure/General/completion.scala
author wenzelm
Wed Nov 01 21:21:09 2017 +0100 (19 months ago)
changeset 66985 7382ff5b46b9
parent 66984 a1d3e5df0c95
child 67004 af72fa58f71b
permissions -rw-r--r--
tuned;
     1 /*  Title:      Pure/General/completion.scala
     2     Author:     Makarius
     3 
     4 Semantic completion within the formal context (reported names).
     5 Syntactic completion of keywords and symbols, with abbreviations
     6 (based on language context).
     7 */
     8 
     9 package isabelle
    10 
    11 
    12 import scala.collection.immutable.SortedMap
    13 import scala.util.parsing.combinator.RegexParsers
    14 import scala.util.matching.Regex
    15 import scala.math.Ordering
    16 
    17 
    18 object Completion
    19 {
    20   /** completion result **/
    21 
    22   sealed case class Item(
    23     range: Text.Range,
    24     original: String,
    25     name: String,
    26     description: List[String],
    27     replacement: String,
    28     move: Int,
    29     immediate: Boolean)
    30 
    31   object Result
    32   {
    33     def empty(range: Text.Range): Result = Result(range, "", false, Nil)
    34     def merge(history: History, results: Option[Result]*): Option[Result] =
    35       ((None: Option[Result]) /: results)({
    36         case (result1, None) => result1
    37         case (None, result2) => result2
    38         case (result1 @ Some(res1), Some(res2)) =>
    39           if (res1.range != res2.range || res1.original != res2.original) result1
    40           else {
    41             val items = (res1.items ::: res2.items).sorted(history.ordering)
    42             Some(Result(res1.range, res1.original, false, items))
    43           }
    44       })
    45   }
    46 
    47   sealed case class Result(
    48     range: Text.Range,
    49     original: String,
    50     unique: Boolean,
    51     items: List[Item])
    52 
    53 
    54 
    55   /** persistent history **/
    56 
    57   private val COMPLETION_HISTORY = Path.explode("$ISABELLE_HOME_USER/etc/completion_history")
    58 
    59   object History
    60   {
    61     val empty: History = new History()
    62 
    63     def load(): History =
    64     {
    65       def ignore_error(msg: String): Unit =
    66         Output.warning("Ignoring bad content of file " + COMPLETION_HISTORY +
    67           (if (msg == "") "" else "\n" + msg))
    68 
    69       val content =
    70         if (COMPLETION_HISTORY.is_file) {
    71           try {
    72             import XML.Decode._
    73             list(pair(string, int))(Symbol.decode_yxml(File.read(COMPLETION_HISTORY)))
    74           }
    75           catch {
    76             case ERROR(msg) => ignore_error(msg); Nil
    77             case _: XML.Error => ignore_error(""); Nil
    78           }
    79         }
    80         else Nil
    81       (empty /: content)(_ + _)
    82     }
    83   }
    84 
    85   final class History private(rep: SortedMap[String, Int] = SortedMap.empty)
    86   {
    87     override def toString: String = rep.mkString("Completion.History(", ",", ")")
    88 
    89     def frequency(name: String): Int =
    90       default_frequency(Symbol.encode(name)) getOrElse
    91       rep.getOrElse(name, 0)
    92 
    93     def + (entry: (String, Int)): History =
    94     {
    95       val (name, freq) = entry
    96       if (name == "") this
    97       else new History(rep + (name -> (frequency(name) + freq)))
    98     }
    99 
   100     def ordering: Ordering[Item] =
   101       new Ordering[Item] {
   102         def compare(item1: Item, item2: Item): Int =
   103           frequency(item2.name) compare frequency(item1.name)
   104       }
   105 
   106     def save()
   107     {
   108       Isabelle_System.mkdirs(COMPLETION_HISTORY.dir)
   109       File.write_backup(COMPLETION_HISTORY,
   110         {
   111           import XML.Encode._
   112           Symbol.encode_yxml(list(pair(string, int))(rep.toList))
   113         })
   114     }
   115   }
   116 
   117   class History_Variable
   118   {
   119     private var history = History.empty
   120     def value: History = synchronized { history }
   121 
   122     def load()
   123     {
   124       val h = History.load()
   125       synchronized { history = h }
   126     }
   127 
   128     def update(item: Item, freq: Int = 1): Unit = synchronized {
   129       history = history + (item.name -> freq)
   130     }
   131   }
   132 
   133 
   134 
   135   /** semantic completion **/
   136 
   137   def clean_name(s: String): Option[String] =
   138     if (s == "" || s == "_") None
   139     else Some(s.reverseIterator.dropWhile(_ == '_').toList.reverse.mkString)
   140 
   141   def completed(input: String): String => Boolean =
   142     clean_name(input) match {
   143       case None => (name: String) => false
   144       case Some(prefix) => (name: String) => name.startsWith(prefix)
   145     }
   146 
   147   def report_no_completion(pos: Position.T): String =
   148     YXML.string_of_tree(Semantic.Info(pos, No_Completion))
   149 
   150   def report_names(pos: Position.T, names: List[(String, (String, String))], total: Int = 0): String =
   151     if (names.isEmpty) ""
   152     else
   153       YXML.string_of_tree(Semantic.Info(pos, Names(if (total > 0) total else names.length, names)))
   154 
   155   def report_theories(pos: Position.T, thys: List[String], total: Int = 0): String =
   156     report_names(pos, thys.map(name => (name, ("theory", name))), total)
   157 
   158   object Semantic
   159   {
   160     object Info
   161     {
   162       def apply(pos: Position.T, semantic: Semantic): XML.Elem =
   163       {
   164         val elem =
   165           semantic match {
   166             case No_Completion => XML.Elem(Markup(Markup.NO_COMPLETION, pos), Nil)
   167             case Names(total, names) =>
   168               XML.Elem(Markup(Markup.COMPLETION, pos),
   169                 {
   170                   import XML.Encode._
   171                   pair(int, list(pair(string, pair(string, string))))(total, names)
   172                 })
   173           }
   174         XML.Elem(Markup(Markup.REPORT, pos), List(elem))
   175       }
   176 
   177       def unapply(info: Text.Markup): Option[Text.Info[Semantic]] =
   178         info.info match {
   179           case XML.Elem(Markup(Markup.COMPLETION, _), body) =>
   180             try {
   181               val (total, names) =
   182               {
   183                 import XML.Decode._
   184                 pair(int, list(pair(string, pair(string, string))))(body)
   185               }
   186               Some(Text.Info(info.range, Names(total, names)))
   187             }
   188             catch { case _: XML.Error => None }
   189           case XML.Elem(Markup(Markup.NO_COMPLETION, _), _) =>
   190             Some(Text.Info(info.range, No_Completion))
   191           case _ => None
   192         }
   193     }
   194   }
   195 
   196   sealed abstract class Semantic
   197   case object No_Completion extends Semantic
   198   case class Names(total: Int, names: List[(String, (String, String))]) extends Semantic
   199   {
   200     def complete(
   201       range: Text.Range,
   202       history: Completion.History,
   203       unicode: Boolean,
   204       original: String): Option[Completion.Result] =
   205     {
   206       def decode(s: String): String = if (unicode) Symbol.decode(s) else s
   207       val items =
   208         for {
   209           (xname, (kind, name)) <- names
   210           xname1 = decode(xname)
   211           if xname1 != original
   212           (full_name, descr_name) =
   213             if (kind == "") (name, quote(decode(name)))
   214             else
   215              (Long_Name.qualify(kind, name),
   216               Word.implode(Word.explode('_', kind)) +
   217               (if (xname == name) "" else " " + quote(decode(name))))
   218         } yield {
   219           val description = List(xname1, "(" + descr_name + ")")
   220           val replacement =
   221             List(original, xname1).map(Token.explode(Keyword.Keywords.empty, _)) match {
   222               case List(List(tok), _) if tok.kind == Token.Kind.CARTOUCHE =>
   223                 Symbol.open_decoded + xname1 + Symbol.close_decoded
   224               case List(_, List(tok)) if tok.is_name => xname1
   225               case _ => quote(xname1)
   226             }
   227           Item(range, original, full_name, description, replacement, 0, true)
   228         }
   229 
   230       if (items.isEmpty) None
   231       else Some(Result(range, original, names.length == 1, items.sorted(history.ordering)))
   232     }
   233   }
   234 
   235 
   236 
   237   /** syntactic completion **/
   238 
   239   /* language context */
   240 
   241   object Language_Context
   242   {
   243     val outer = Language_Context("", true, false)
   244     val inner = Language_Context(Markup.Language.UNKNOWN, true, false)
   245     val ML_outer = Language_Context(Markup.Language.ML, false, true)
   246     val ML_inner = Language_Context(Markup.Language.ML, true, false)
   247     val SML_outer = Language_Context(Markup.Language.SML, false, false)
   248   }
   249 
   250   sealed case class Language_Context(language: String, symbols: Boolean, antiquotes: Boolean)
   251   {
   252     def is_outer: Boolean = language == ""
   253   }
   254 
   255 
   256   /* init */
   257 
   258   val empty: Completion = new Completion()
   259 
   260   lazy val init: Completion =
   261     empty.add_symbols.add_abbrevs(Completion.symbol_abbrevs ::: Completion.default_abbrevs)
   262 
   263 
   264   /* word parsers */
   265 
   266   object Word_Parsers extends RegexParsers
   267   {
   268     override val whiteSpace = "".r
   269 
   270     private val symboloid_regex: Regex = """\\([A-Za-z0-9_']+|<\^?[A-Za-z0-9_']+>?)""".r
   271     def is_symboloid(s: CharSequence): Boolean = symboloid_regex.pattern.matcher(s).matches
   272 
   273     private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
   274     private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
   275     private def reverse_escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
   276 
   277     private val word_regex = "[a-zA-Z0-9_'.]+".r
   278     private def word2: Parser[String] = "[a-zA-Z0-9_'.]{2,}".r
   279     private def underscores: Parser[String] = "_*".r
   280 
   281     def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
   282     def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.'
   283 
   284     def read_symbol(in: CharSequence): Option[String] =
   285     {
   286       val reverse_in = new Library.Reverse(in)
   287       parse(reverse_symbol ^^ (_.reverse), reverse_in) match {
   288         case Success(result, _) => Some(result)
   289         case _ => None
   290       }
   291     }
   292 
   293     def read_word(in: CharSequence): Option[(String, String)] =
   294     {
   295       val reverse_in = new Library.Reverse(in)
   296       val parser =
   297         (reverse_symbol | reverse_symb | reverse_escape) ^^ (x => (x.reverse, "")) |
   298         underscores ~ word2 ~ opt("?") ^^
   299         { case x ~ y ~ z => (z.getOrElse("") + y.reverse, x) }
   300       parse(parser, reverse_in) match {
   301         case Success(result, _) => Some(result)
   302         case _ => None
   303       }
   304     }
   305   }
   306 
   307 
   308   /* templates */
   309 
   310   val caret_indicator = '\u0007'
   311 
   312   def split_template(s: String): (String, String) =
   313     space_explode(caret_indicator, s) match {
   314       case List(s1, s2) => (s1, s2)
   315       case _ => (s, "")
   316     }
   317 
   318 
   319   /* abbreviations */
   320 
   321   private def symbol_abbrevs: Thy_Header.Abbrevs =
   322     for ((sym, abbr) <- Symbol.abbrevs.toList) yield (abbr, sym)
   323 
   324   private val antiquote = "@{"
   325 
   326   private val default_abbrevs =
   327     List("@{" -> "@{\u0007}",
   328       "`" -> "\\<close>",
   329       "`" -> "\\<open>",
   330       "`" -> "\\<open>\u0007\\<close>",
   331       "\"" -> "\\<close>",
   332       "\"" -> "\\<open>",
   333       "\"" -> "\\<open>\u0007\\<close>")
   334 
   335   private def default_frequency(name: String): Option[Int] =
   336     default_abbrevs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2)
   337 }
   338 
   339 final class Completion private(
   340   protected val keywords: Set[String] = Set.empty,
   341   protected val words_lex: Scan.Lexicon = Scan.Lexicon.empty,
   342   protected val words_map: Multi_Map[String, String] = Multi_Map.empty,
   343   protected val abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
   344   protected val abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty)
   345 {
   346   /* merge */
   347 
   348   def is_empty: Boolean =
   349     keywords.isEmpty &&
   350     words_lex.is_empty &&
   351     words_map.isEmpty &&
   352     abbrevs_lex.is_empty &&
   353     abbrevs_map.isEmpty
   354 
   355   def ++ (other: Completion): Completion =
   356     if (this eq other) this
   357     else if (is_empty) other
   358     else {
   359       val keywords1 =
   360         if (keywords eq other.keywords) keywords
   361         else if (keywords.isEmpty) other.keywords
   362         else (keywords /: other.keywords) { case (ks, k) => if (ks(k)) ks else ks + k }
   363       val words_lex1 = words_lex ++ other.words_lex
   364       val words_map1 = words_map ++ other.words_map
   365       val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex
   366       val abbrevs_map1 = abbrevs_map ++ other.abbrevs_map
   367       if ((keywords eq keywords1) && (words_lex eq words_lex1) && (words_map eq words_map1) &&
   368         (abbrevs_lex eq abbrevs_lex1) && (abbrevs_map eq abbrevs_map1)) this
   369       else new Completion(keywords1, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
   370     }
   371 
   372 
   373   /* keywords */
   374 
   375   private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
   376   private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords(name)
   377   private def is_keyword_template(name: String, template: Boolean): Boolean =
   378     is_keyword(name) && (words_map.getOrElse(name, name) != name) == template
   379 
   380   def add_keyword(keyword: String): Completion =
   381     new Completion(keywords + keyword, words_lex, words_map, abbrevs_lex, abbrevs_map)
   382 
   383 
   384   /* symbols and abbrevs */
   385 
   386   def add_symbols: Completion =
   387   {
   388     val words =
   389       (for ((sym, _) <- Symbol.names.toList) yield (sym, sym)) :::
   390       (for ((sym, name) <- Symbol.names.toList) yield ("\\" + name, sym))
   391 
   392     new Completion(
   393       keywords,
   394       words_lex ++ words.map(_._1),
   395       words_map ++ words,
   396       abbrevs_lex,
   397       abbrevs_map)
   398   }
   399 
   400   def add_abbrevs(abbrevs: List[(String, String)]): Completion =
   401     (this /: abbrevs)(_.add_abbrev(_))
   402 
   403   private def add_abbrev(abbrev: (String, String)): Completion =
   404     abbrev match {
   405       case ("", _) => this
   406       case (abbr, text) =>
   407         val rev_abbr = abbr.reverse
   408         val is_word = Completion.Word_Parsers.is_word(abbr)
   409 
   410         val (words_lex1, words_map1) =
   411           if (!is_word) (words_lex, words_map)
   412           else if (text != "") (words_lex + abbr, words_map + abbrev)
   413           else (words_lex -- List(abbr), words_map - abbr)
   414 
   415         val (abbrevs_lex1, abbrevs_map1) =
   416           if (is_word) (abbrevs_lex, abbrevs_map)
   417           else if (text != "") (abbrevs_lex + rev_abbr, abbrevs_map + (rev_abbr -> abbrev))
   418           else (abbrevs_lex -- List(rev_abbr), abbrevs_map - rev_abbr)
   419 
   420         new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
   421     }
   422 
   423 
   424   /* complete */
   425 
   426   def complete(
   427     history: Completion.History,
   428     unicode: Boolean,
   429     explicit: Boolean,
   430     start: Text.Offset,
   431     text: CharSequence,
   432     caret: Int,
   433     language_context: Completion.Language_Context): Option[Completion.Result] =
   434   {
   435     val length = text.length
   436 
   437     val abbrevs_result =
   438     {
   439       val reverse_in = new Library.Reverse(text.subSequence(0, caret))
   440       Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), reverse_in) match {
   441         case Scan.Parsers.Success(reverse_abbr, _) =>
   442           val abbrevs = abbrevs_map.get_list(reverse_abbr)
   443           abbrevs match {
   444             case Nil => None
   445             case (abbr, _) :: _ =>
   446               val ok =
   447                 if (abbr == Completion.antiquote) language_context.antiquotes
   448                 else language_context.symbols || Completion.default_abbrevs.exists(_._1 == abbr)
   449               if (ok) Some((abbr, abbrevs))
   450               else None
   451           }
   452         case _ => None
   453       }
   454     }
   455 
   456     val words_result =
   457       if (abbrevs_result.isDefined) None
   458       else {
   459         val word_context =
   460           caret < length && Completion.Word_Parsers.is_word_char(text.charAt(caret))
   461         val result =
   462           Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) match {
   463             case Some(symbol) => Some((symbol, ""))
   464             case None => Completion.Word_Parsers.read_word(text.subSequence(0, caret))
   465           }
   466         result.map(
   467           {
   468             case (word, underscores) =>
   469               val complete_words = words_lex.completions(word)
   470               val full_word = word + underscores
   471               val completions =
   472                 if (complete_words.contains(full_word) && is_keyword_template(full_word, false)) Nil
   473                 else
   474                   for {
   475                     complete_word <- complete_words
   476                     ok =
   477                       if (is_keyword(complete_word)) !word_context && language_context.is_outer
   478                       else language_context.symbols || Completion.Word_Parsers.is_symboloid(word)
   479                     if ok
   480                     completion <- words_map.get_list(complete_word)
   481                   } yield (complete_word, completion)
   482               (full_word, completions)
   483           })
   484       }
   485 
   486     (abbrevs_result orElse words_result) match {
   487       case Some((original, completions)) if completions.nonEmpty =>
   488         val range = Text.Range(- original.length, 0) + caret + start
   489         val immediate =
   490           explicit ||
   491             (!Completion.Word_Parsers.is_word(original) &&
   492              !Completion.Word_Parsers.is_symboloid(original) &&
   493               Character.codePointCount(original, 0, original.length) > 1)
   494         val unique = completions.length == 1
   495 
   496         def decode1(s: String): String = if (unicode) Symbol.decode(s) else s
   497         def decode2(s: String): String = if (unicode) s else Symbol.decode(s)
   498 
   499         val items =
   500           for {
   501             (complete_word, name0) <- completions
   502             name1 = decode1(name0)
   503             name2 = decode2(name0)
   504             if name1 != original
   505             (s1, s2) = Completion.split_template(name1)
   506             move = - s2.length
   507             description =
   508               if (is_symbol(name0)) {
   509                 if (name1 == name2) List(name1)
   510                 else List(name1, "(symbol " + quote(name2) + ")")
   511               }
   512               else if (is_keyword_template(complete_word, true))
   513                 List(name1, "(template " + quote(complete_word) + ")")
   514               else if (move != 0) List(name1, "(template)")
   515               else if (is_keyword(complete_word)) List(name1, "(keyword)")
   516               else List(name1)
   517           }
   518           yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)
   519 
   520         if (items.isEmpty) None
   521         else
   522           Some(Completion.Result(range, original, unique,
   523             items.sortBy(_.name).sorted(history.ordering)))
   524 
   525       case _ => None
   526     }
   527   }
   528 }