1/* Title: Pure/General/completion.scala 2 Author: Makarius 3 4Semantic completion within the formal context (reported names). 5Syntactic completion of keywords and symbols, with abbreviations 6(based on language context). 7*/ 8 9package isabelle 10 11 12import scala.collection.immutable.SortedMap 13import scala.util.parsing.combinator.RegexParsers 14import scala.util.matching.Regex 15import scala.math.Ordering 16 17 18object 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.cartouche_decoded(xname1) 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 /* make */ 257 258 val empty: Completion = new Completion() 259 260 def make(keywords: List[String], abbrevs: List[(String, String)]): Completion = 261 empty.add_symbols.add_keywords(keywords).add_abbrevs( 262 Completion.symbol_abbrevs ::: Completion.default_abbrevs ::: abbrevs) 263 264 265 /* word parsers */ 266 267 object Word_Parsers extends RegexParsers 268 { 269 override val whiteSpace = "".r 270 271 private val symboloid_regex: Regex = """\\([A-Za-z0-9_']+|<\^?[A-Za-z0-9_']+>?)""".r 272 def is_symboloid(s: CharSequence): Boolean = symboloid_regex.pattern.matcher(s).matches 273 274 private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r 275 private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r 276 private def reverse_escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r 277 278 private val word_regex = "[a-zA-Z0-9_'.]+".r 279 private def word2: Parser[String] = "[a-zA-Z0-9_'.]{2,}".r 280 private def underscores: Parser[String] = "_*".r 281 282 def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches 283 def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.' 284 285 def read_symbol(in: CharSequence): Option[String] = 286 { 287 val reverse_in = new Library.Reverse(in) 288 parse(reverse_symbol ^^ (_.reverse), reverse_in) match { 289 case Success(result, _) => Some(result) 290 case _ => None 291 } 292 } 293 294 def read_word(in: CharSequence): Option[(String, String)] = 295 { 296 val reverse_in = new Library.Reverse(in) 297 val parser = 298 (reverse_symbol | reverse_symb | reverse_escape) ^^ (x => (x.reverse, "")) | 299 underscores ~ word2 ~ opt("?") ^^ 300 { case x ~ y ~ z => (z.getOrElse("") + y.reverse, x) } 301 parse(parser, reverse_in) match { 302 case Success(result, _) => Some(result) 303 case _ => None 304 } 305 } 306 } 307 308 309 /* templates */ 310 311 val caret_indicator = '\u0007' 312 313 def split_template(s: String): (String, String) = 314 space_explode(caret_indicator, s) match { 315 case List(s1, s2) => (s1, s2) 316 case _ => (s, "") 317 } 318 319 320 /* abbreviations */ 321 322 private def symbol_abbrevs: Thy_Header.Abbrevs = 323 for ((sym, abbr) <- Symbol.abbrevs.toList) yield (abbr, sym) 324 325 private val antiquote = "@{" 326 327 private val default_abbrevs = 328 List("@{" -> "@{\u0007}", 329 "`" -> "\\<close>", 330 "`" -> "\\<open>", 331 "`" -> "\\<open>\u0007\\<close>", 332 "\"" -> "\\<close>", 333 "\"" -> "\\<open>", 334 "\"" -> "\\<open>\u0007\\<close>") 335 336 private def default_frequency(name: String): Option[Int] = 337 default_abbrevs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2) 338} 339 340final class Completion private( 341 keywords: Set[String] = Set.empty, 342 words_lex: Scan.Lexicon = Scan.Lexicon.empty, 343 words_map: Multi_Map[String, String] = Multi_Map.empty, 344 abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty, 345 abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty) 346{ 347 /* keywords */ 348 349 private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name) 350 private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords(name) 351 private def is_keyword_template(name: String, template: Boolean): Boolean = 352 is_keyword(name) && (words_map.getOrElse(name, name) != name) == template 353 354 def add_keyword(keyword: String): Completion = 355 new Completion(keywords + keyword, words_lex, words_map, abbrevs_lex, abbrevs_map) 356 357 def add_keywords(names: List[String]): Completion = 358 { 359 val keywords1 = (keywords /: names) { case (ks, k) => if (ks(k)) ks else ks + k } 360 if (keywords eq keywords1) this 361 else new Completion(keywords1, words_lex, words_map, abbrevs_lex, abbrevs_map) 362 } 363 364 365 /* symbols and abbrevs */ 366 367 def add_symbols: Completion = 368 { 369 val words = 370 Symbol.names.toList.flatMap({ case (sym, (name, argument)) => 371 val word = "\\" + name 372 val seps = 373 if (argument == Symbol.ARGUMENT_CARTOUCHE) List("") 374 else if (argument == Symbol.ARGUMENT_SPACE_CARTOUCHE) List(" ") 375 else Nil 376 List(sym -> sym, word -> sym) ::: 377 seps.map(sep => word -> (sym + sep + "\\<open>\u0007\\<close>")) 378 }) 379 380 new Completion( 381 keywords, 382 words_lex ++ words.map(_._1), 383 words_map ++ words, 384 abbrevs_lex, 385 abbrevs_map) 386 } 387 388 def add_abbrevs(abbrevs: List[(String, String)]): Completion = 389 (this /: abbrevs)(_.add_abbrev(_)) 390 391 private def add_abbrev(abbrev: (String, String)): Completion = 392 abbrev match { 393 case ("", _) => this 394 case (abbr, text) => 395 val rev_abbr = abbr.reverse 396 val is_word = Completion.Word_Parsers.is_word(abbr) 397 398 val (words_lex1, words_map1) = 399 if (!is_word) (words_lex, words_map) 400 else if (text != "") (words_lex + abbr, words_map + abbrev) 401 else (words_lex -- List(abbr), words_map - abbr) 402 403 val (abbrevs_lex1, abbrevs_map1) = 404 if (is_word) (abbrevs_lex, abbrevs_map) 405 else if (text != "") (abbrevs_lex + rev_abbr, abbrevs_map + (rev_abbr -> abbrev)) 406 else (abbrevs_lex -- List(rev_abbr), abbrevs_map - rev_abbr) 407 408 new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1) 409 } 410 411 412 /* complete */ 413 414 def complete( 415 history: Completion.History, 416 unicode: Boolean, 417 explicit: Boolean, 418 start: Text.Offset, 419 text: CharSequence, 420 caret: Int, 421 language_context: Completion.Language_Context): Option[Completion.Result] = 422 { 423 val length = text.length 424 425 val abbrevs_result = 426 { 427 val reverse_in = new Library.Reverse(text.subSequence(0, caret)) 428 Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), reverse_in) match { 429 case Scan.Parsers.Success(reverse_abbr, _) => 430 val abbrevs = abbrevs_map.get_list(reverse_abbr) 431 abbrevs match { 432 case Nil => None 433 case (abbr, _) :: _ => 434 val ok = 435 if (abbr == Completion.antiquote) language_context.antiquotes 436 else language_context.symbols || Completion.default_abbrevs.exists(_._1 == abbr) 437 if (ok) Some((abbr, abbrevs)) 438 else None 439 } 440 case _ => None 441 } 442 } 443 444 val words_result = 445 if (abbrevs_result.isDefined) None 446 else { 447 val word_context = 448 caret < length && Completion.Word_Parsers.is_word_char(text.charAt(caret)) 449 val result = 450 Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) match { 451 case Some(symbol) => Some((symbol, "")) 452 case None => Completion.Word_Parsers.read_word(text.subSequence(0, caret)) 453 } 454 result.map( 455 { 456 case (word, underscores) => 457 val complete_words = words_lex.completions(word) 458 val full_word = word + underscores 459 val completions = 460 if (complete_words.contains(full_word) && is_keyword_template(full_word, false)) Nil 461 else 462 for { 463 complete_word <- complete_words 464 ok = 465 if (is_keyword(complete_word)) !word_context && language_context.is_outer 466 else language_context.symbols || Completion.Word_Parsers.is_symboloid(word) 467 if ok 468 completion <- words_map.get_list(complete_word) 469 } yield (complete_word, completion) 470 (full_word, completions) 471 }) 472 } 473 474 (abbrevs_result orElse words_result) match { 475 case Some((original, completions)) if completions.nonEmpty => 476 val range = Text.Range(- original.length, 0) + caret + start 477 val immediate = 478 explicit || 479 (!Completion.Word_Parsers.is_word(original) && 480 !Completion.Word_Parsers.is_symboloid(original) && 481 Character.codePointCount(original, 0, original.length) > 1) 482 val unique = completions.length == 1 483 484 def decode1(s: String): String = if (unicode) Symbol.decode(s) else s 485 def decode2(s: String): String = if (unicode) s else Symbol.decode(s) 486 487 val items = 488 for { 489 (complete_word, name0) <- completions 490 name1 = decode1(name0) 491 name2 = decode2(name0) 492 if name1 != original 493 (s1, s2) = Completion.split_template(name1) 494 move = - s2.length 495 description = 496 if (is_symbol(name0)) { 497 if (name1 == name2) List(name1) 498 else List(name1, "(symbol " + quote(name2) + ")") 499 } 500 else if (is_keyword_template(complete_word, true)) 501 List(name1, "(template " + quote(complete_word) + ")") 502 else if (move != 0) List(name1, "(template)") 503 else if (is_keyword(complete_word)) List(name1, "(keyword)") 504 else List(name1) 505 } 506 yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate) 507 508 if (items.isEmpty) None 509 else 510 Some(Completion.Result(range, original, unique, 511 items.sortBy(_.name).sorted(history.ordering))) 512 513 case _ => None 514 } 515 } 516} 517