src/Pure/General/completion.scala
author wenzelm
Mon Dec 01 15:21:49 2014 +0100 (2014-12-01)
changeset 59073 dcecfcc56dce
parent 57602 0f708666eb7c
child 59319 677615cba30d
permissions -rw-r--r--
more merge operations;
     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, result1: Option[Result], result2: Option[Result]): Option[Result] =
    35       (result1, result2) match {
    36         case (_, None) => result1
    37         case (None, _) => result2
    38         case (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(Symbol.decode_string, int))(
    74               YXML.parse_body(File.read(COMPLETION_HISTORY)))
    75           }
    76           catch {
    77             case ERROR(msg) => ignore_error(msg); Nil
    78             case _: XML.Error => ignore_error(""); Nil
    79           }
    80         }
    81         else Nil
    82       (empty /: content)(_ + _)
    83     }
    84   }
    85 
    86   final class History private(rep: SortedMap[String, Int] = SortedMap.empty)
    87   {
    88     override def toString: String = rep.mkString("Completion.History(", ",", ")")
    89 
    90     def frequency(name: String): Int =
    91       default_frequency(Symbol.encode(name)) getOrElse
    92       rep.getOrElse(name, 0)
    93 
    94     def + (entry: (String, Int)): History =
    95     {
    96       val (name, freq) = entry
    97       if (name == "") this
    98       else new History(rep + (name -> (frequency(name) + freq)))
    99     }
   100 
   101     def ordering: Ordering[Item] =
   102       new Ordering[Item] {
   103         def compare(item1: Item, item2: Item): Int =
   104           frequency(item2.name) compare frequency(item1.name)
   105       }
   106 
   107     def save()
   108     {
   109       Isabelle_System.mkdirs(COMPLETION_HISTORY.dir)
   110       File.write_backup(COMPLETION_HISTORY,
   111         {
   112           import XML.Encode._
   113           YXML.string_of_body(list(pair(Symbol.encode_string, int))(rep.toList))
   114         })
   115     }
   116   }
   117 
   118   class History_Variable
   119   {
   120     private var history = History.empty
   121     def value: History = synchronized { history }
   122 
   123     def load()
   124     {
   125       val h = History.load()
   126       synchronized { history = h }
   127     }
   128 
   129     def update(item: Item, freq: Int = 1): Unit = synchronized {
   130       history = history + (item.name -> freq)
   131     }
   132   }
   133 
   134 
   135 
   136   /** semantic completion **/
   137 
   138   object Semantic
   139   {
   140     object Info
   141     {
   142       def unapply(info: Text.Markup): Option[Text.Info[Semantic]] =
   143         info.info match {
   144           case XML.Elem(Markup(Markup.COMPLETION, _), body) =>
   145             try {
   146               val (total, names) =
   147               {
   148                 import XML.Decode._
   149                 pair(int, list(pair(string, pair(string, string))))(body)
   150               }
   151               Some(Text.Info(info.range, Names(total, names)))
   152             }
   153             catch { case _: XML.Error => None }
   154           case XML.Elem(Markup(Markup.NO_COMPLETION, _), _) =>
   155             Some(Text.Info(info.range, No_Completion))
   156           case _ => None
   157         }
   158     }
   159   }
   160 
   161   sealed abstract class Semantic
   162   case object No_Completion extends Semantic
   163   case class Names(total: Int, names: List[(String, (String, String))]) extends Semantic
   164   {
   165     def complete(
   166       range: Text.Range,
   167       history: Completion.History,
   168       do_decode: Boolean,
   169       original: String): Option[Completion.Result] =
   170     {
   171       def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
   172       val items =
   173         for {
   174           (xname, (kind, name)) <- names
   175           xname1 = decode(xname)
   176           if xname1 != original
   177           (full_name, descr_name) =
   178             if (kind == "") (name, quote(decode(name)))
   179             else
   180              (Long_Name.qualify(kind, name),
   181               Word.implode(Word.explode('_', kind)) + " " + quote(decode(name)))
   182           description = List(xname1, "(" + descr_name + ")")
   183         } yield Item(range, original, full_name, description, xname1, 0, true)
   184 
   185       if (items.isEmpty) None
   186       else Some(Result(range, original, names.length == 1, items.sorted(history.ordering)))
   187     }
   188   }
   189 
   190 
   191 
   192   /** syntactic completion **/
   193 
   194   /* language context */
   195 
   196   object Language_Context
   197   {
   198     val outer = Language_Context("", true, false)
   199     val inner = Language_Context(Markup.Language.UNKNOWN, true, false)
   200     val ML_outer = Language_Context(Markup.Language.ML, false, true)
   201     val ML_inner = Language_Context(Markup.Language.ML, true, false)
   202     val SML_outer = Language_Context(Markup.Language.SML, false, false)
   203   }
   204 
   205   sealed case class Language_Context(language: String, symbols: Boolean, antiquotes: Boolean)
   206   {
   207     def is_outer: Boolean = language == ""
   208   }
   209 
   210 
   211   /* init */
   212 
   213   val empty: Completion = new Completion()
   214   def init(): Completion = empty.add_symbols()
   215 
   216 
   217   /* word parsers */
   218 
   219   private object Word_Parsers extends RegexParsers
   220   {
   221     override val whiteSpace = "".r
   222 
   223     private val symbol_regex: Regex = """\\<\^?[A-Za-z0-9_']+>""".r
   224     def is_symbol(s: CharSequence): Boolean = symbol_regex.pattern.matcher(s).matches
   225 
   226     private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
   227     private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
   228     private def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
   229 
   230     private val word_regex = "[a-zA-Z0-9_'.]+".r
   231     private def word: Parser[String] = word_regex
   232     private def word3: Parser[String] = "[a-zA-Z0-9_'.]{3,}".r
   233     private def underscores: Parser[String] = "_*".r
   234 
   235     def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
   236     def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.'
   237 
   238     def read_symbol(in: CharSequence): Option[String] =
   239     {
   240       val reverse_in = new Library.Reverse(in)
   241       parse(reverse_symbol ^^ (_.reverse), reverse_in) match {
   242         case Success(result, _) => Some(result)
   243         case _ => None
   244       }
   245     }
   246 
   247     def read_word(explicit: Boolean, in: CharSequence): Option[(String, String)] =
   248     {
   249       val parse_word = if (explicit) word else word3
   250       val reverse_in = new Library.Reverse(in)
   251       val parser =
   252         (reverse_symbol | reverse_symb | escape) ^^ (x => (x.reverse, "")) |
   253         underscores ~ parse_word ~ opt("?") ^^
   254         { case x ~ y ~ z => (z.getOrElse("") + y.reverse, x) }
   255       parse(parser, reverse_in) match {
   256         case Success(result, _) => Some(result)
   257         case _ => None
   258       }
   259     }
   260   }
   261 
   262 
   263   /* abbreviations */
   264 
   265   private val caret_indicator = '\u0007'
   266   private val antiquote = "@{"
   267 
   268   private val default_abbrs =
   269     List("@{" -> "@{\u0007}",
   270       "`" -> "\\<close>",
   271       "`" -> "\\<open>",
   272       "`" -> "\\<open>\u0007\\<close>")
   273 
   274   private def default_frequency(name: String): Option[Int] =
   275     default_abbrs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2)
   276 }
   277 
   278 final class Completion private(
   279   protected val keywords: Map[String, Boolean] = Map.empty,
   280   protected val words_lex: Scan.Lexicon = Scan.Lexicon.empty,
   281   protected val words_map: Multi_Map[String, String] = Multi_Map.empty,
   282   protected val abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
   283   protected val abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty)
   284 {
   285   /* merge */
   286 
   287   def is_empty: Boolean =
   288     keywords.isEmpty &&
   289     words_lex.is_empty &&
   290     words_map.isEmpty &&
   291     abbrevs_lex.is_empty &&
   292     abbrevs_map.isEmpty
   293 
   294   def ++ (other: Completion): Completion =
   295     if (this eq other) this
   296     else if (is_empty) other
   297     else {
   298       val keywords1 =
   299         (keywords /: other.keywords) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
   300       val words_lex1 = words_lex ++ other.words_lex
   301       val words_map1 = words_map ++ other.words_map
   302       val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex
   303       val abbrevs_map1 = abbrevs_map ++ other.abbrevs_map
   304       new Completion(keywords1, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
   305     }
   306 
   307 
   308   /* keywords */
   309 
   310   private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
   311   private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords.isDefinedAt(name)
   312   private def is_keyword_template(name: String, template: Boolean): Boolean =
   313     is_keyword(name) && keywords(name) == template
   314 
   315   def + (keyword: String, template: String): Completion =
   316     new Completion(
   317       keywords + (keyword -> (keyword != template)),
   318       words_lex + keyword,
   319       words_map + (keyword -> template),
   320       abbrevs_lex,
   321       abbrevs_map)
   322 
   323   def + (keyword: String): Completion = this + (keyword, keyword)
   324 
   325 
   326   /* symbols with abbreviations */
   327 
   328   private def add_symbols(): Completion =
   329   {
   330     val words =
   331       (for ((x, _) <- Symbol.names.toList) yield (x, x)) :::
   332       (for ((x, y) <- Symbol.names.toList) yield ("\\" + y, x)) :::
   333       (for ((x, y) <- Symbol.abbrevs.toList if Completion.Word_Parsers.is_word(y)) yield (y, x))
   334 
   335     val symbol_abbrs =
   336       (for ((x, y) <- Symbol.abbrevs.iterator if !Completion.Word_Parsers.is_word(y))
   337         yield (y, x)).toList
   338 
   339     val abbrs =
   340       for ((a, b) <- symbol_abbrs ::: Completion.default_abbrs)
   341         yield (a.reverse, (a, b))
   342 
   343     new Completion(
   344       keywords,
   345       words_lex ++ words.map(_._1),
   346       words_map ++ words,
   347       abbrevs_lex ++ abbrs.map(_._1),
   348       abbrevs_map ++ abbrs)
   349   }
   350 
   351 
   352   /* complete */
   353 
   354   def complete(
   355     history: Completion.History,
   356     do_decode: Boolean,
   357     explicit: Boolean,
   358     start: Text.Offset,
   359     text: CharSequence,
   360     caret: Int,
   361     language_context: Completion.Language_Context): Option[Completion.Result] =
   362   {
   363     def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
   364     val length = text.length
   365 
   366     val abbrevs_result =
   367     {
   368       val reverse_in = new Library.Reverse(text.subSequence(0, caret))
   369       Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), reverse_in) match {
   370         case Scan.Parsers.Success(reverse_a, _) =>
   371           val abbrevs = abbrevs_map.get_list(reverse_a)
   372           abbrevs match {
   373             case Nil => None
   374             case (a, _) :: _ =>
   375               val ok =
   376                 if (a == Completion.antiquote) language_context.antiquotes
   377                 else
   378                   language_context.symbols ||
   379                   Completion.default_abbrs.exists(_._1 == a) ||
   380                   Completion.Word_Parsers.is_symbol(a)
   381               if (ok) Some((a, abbrevs))
   382               else None
   383           }
   384         case _ => None
   385       }
   386     }
   387 
   388     val words_result =
   389       if (abbrevs_result.isDefined) None
   390       else {
   391         val word_context =
   392           caret < length && Completion.Word_Parsers.is_word_char(text.charAt(caret))
   393         val result =
   394           Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) match {
   395             case Some(symbol) => Some((symbol, ""))
   396             case None => Completion.Word_Parsers.read_word(explicit, text.subSequence(0, caret))
   397           }
   398         result.map(
   399           {
   400             case (word, underscores) =>
   401               val complete_words = words_lex.completions(word)
   402               val full_word = word + underscores
   403               val completions =
   404                 if (complete_words.contains(full_word) && is_keyword_template(full_word, false)) Nil
   405                 else
   406                   for {
   407                     complete_word <- complete_words
   408                     ok =
   409                       if (is_keyword(complete_word)) !word_context && language_context.is_outer
   410                       else language_context.symbols
   411                     if ok
   412                     completion <- words_map.get_list(complete_word)
   413                   } yield (complete_word, completion)
   414               ((full_word, completions))
   415           })
   416       }
   417 
   418     (abbrevs_result orElse words_result) match {
   419       case Some((original, completions)) if !completions.isEmpty =>
   420         val range = Text.Range(- original.length, 0) + caret + start
   421         val immediate =
   422           explicit ||
   423             (!Completion.Word_Parsers.is_word(original) &&
   424               Character.codePointCount(original, 0, original.length) > 1)
   425         val unique = completions.length == 1
   426 
   427         val items =
   428           for {
   429             (complete_word, name0) <- completions
   430             name1 = decode(name0)
   431             if name1 != original
   432             (s1, s2) =
   433               space_explode(Completion.caret_indicator, name1) match {
   434                 case List(s1, s2) => (s1, s2)
   435                 case _ => (name1, "")
   436               }
   437             move = - s2.length
   438             description =
   439               if (is_symbol(name0)) {
   440                 if (name0 == name1) List(name0)
   441                 else List(name1, "(symbol " + quote(name0) + ")")
   442               }
   443               else if (is_keyword_template(complete_word, true))
   444                 List(name1, "(template " + quote(complete_word) + ")")
   445               else if (move != 0) List(name1, "(template)")
   446               else if (is_keyword(complete_word)) List(name1, "(keyword)")
   447               else List(name1)
   448           }
   449           yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)
   450 
   451         if (items.isEmpty) None
   452         else
   453           Some(Completion.Result(range, original, unique,
   454             items.sortBy(_.name).sorted(history.ordering)))
   455 
   456       case _ => None
   457     }
   458   }
   459 }