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