# HG changeset patch # User wenzelm # Date 1392897192 -3600 # Node ID bf4bbe72f740e4b935499477b5e3568d9bbf482d # Parent e2d71b8b0d954c27843111269f1927551ff9dcaf completion of keywords and symbols based on language context; diff -r e2d71b8b0d95 -r bf4bbe72f740 src/Pure/Isar/completion.scala --- a/src/Pure/Isar/completion.scala Wed Feb 19 21:38:44 2014 +0100 +++ b/src/Pure/Isar/completion.scala Thu Feb 20 12:53:12 2014 +0100 @@ -13,6 +13,19 @@ object Completion { + /* context */ + + object Context + { + val default = Context("", true) + } + + sealed case class Context(language: String, symbols: Boolean) + { + def is_outer: Boolean = language == "" + } + + /* result */ sealed case class Item( @@ -113,20 +126,22 @@ } - /** word completion **/ + /** word parsers **/ - private val word_regex = "[a-zA-Z0-9_']+".r - private def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches - - private object Parse extends RegexParsers + private object Word_Parsers extends RegexParsers { override val whiteSpace = "".r - def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r - def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r - def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r - def word: Parser[String] = word_regex - def word3: Parser[String] = """[a-zA-Z0-9_']{3,}""".r + private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r + private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r + private def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r + + private val word_regex = "[a-zA-Z0-9_']+".r + private def word: Parser[String] = word_regex + private def word3: Parser[String] = """[a-zA-Z0-9_']{3,}""".r + + def is_word(s: CharSequence): Boolean = + word_regex.pattern.matcher(s).matches def read(explicit: Boolean, in: CharSequence): Option[String] = { @@ -141,6 +156,7 @@ } final class Completion private( + keywords: Set[String] = Set.empty, words_lex: Scan.Lexicon = Scan.Lexicon.empty, words_map: Multi_Map[String, String] = Multi_Map.empty, abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty, @@ -150,6 +166,7 @@ def + (keyword: String, replace: String): Completion = new Completion( + keywords + keyword, words_lex + keyword, words_map + (keyword -> replace), abbrevs_lex, @@ -160,15 +177,16 @@ private def add_symbols(): Completion = { val words = - (for ((x, _) <- Symbol.names) yield (x, x)).toList ::: - (for ((x, y) <- Symbol.names) yield ("\\" + y, x)).toList ::: - (for ((x, y) <- Symbol.abbrevs.iterator if Completion.is_word(y)) yield (y, x)).toList + (for ((x, _) <- Symbol.names.toList) yield (x, x)) ::: + (for ((x, y) <- Symbol.names.toList) yield ("\\" + y, x)) ::: + (for ((x, y) <- Symbol.abbrevs.toList if Completion.Word_Parsers.is_word(y)) yield (y, x)) val abbrs = - (for ((x, y) <- Symbol.abbrevs.iterator if !Completion.is_word(y)) - yield (y.reverse.toString, (y, x))).toList + (for ((x, y) <- Symbol.abbrevs.iterator if !Completion.Word_Parsers.is_word(y)) + yield (y.reverse, (y, x))).toList new Completion( + keywords, words_lex ++ words.map(_._1), words_map ++ words, abbrevs_lex ++ abbrs.map(_._1), @@ -182,34 +200,45 @@ history: Completion.History, decode: Boolean, explicit: Boolean, - line: CharSequence): Option[Completion.Result] = + text: CharSequence, + context: Completion.Context): Option[Completion.Result] = { - val raw_result = - Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), new Library.Reverse(line)) match { - case Scan.Parsers.Success(reverse_a, _) => - val abbrevs = abbrevs_map.get_list(reverse_a) - abbrevs match { - case Nil => None - case (a, _) :: _ => Some((a, abbrevs.map(_._2))) - } - case _ => - Completion.Parse.read(explicit, line) match { - case Some(word) => - words_lex.completions(word).map(words_map.get_list(_)).flatten match { - case Nil => None - case cs => Some(word, cs) - } - case None => None - } + val abbrevs_result = + if (context.symbols) + Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), new Library.Reverse(text)) match { + case Scan.Parsers.Success(reverse_a, _) => + val abbrevs = abbrevs_map.get_list(reverse_a) + abbrevs match { + case Nil => None + case (a, _) :: _ => Some((a, abbrevs.map(_._2))) + } + case _ => None + } + else None + + val words_result = + abbrevs_result orElse { + Completion.Word_Parsers.read(explicit, text) match { + case Some(word) => + val completions = + for { + s <- words_lex.completions(word) + if (if (keywords(s)) context.is_outer else context.symbols) + r <- words_map.get_list(s) + } yield r + if (completions.isEmpty) None + else Some(word, completions) + case None => None + } } - raw_result match { + + words_result match { case Some((word, cs)) => - val ds = - (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word) + val ds = (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word) if (ds.isEmpty) None else { val immediate = - !Completion.is_word(word) && + !Completion.Word_Parsers.is_word(word) && Character.codePointCount(word, 0, word.length) > 1 val items = ds.map(s => Completion.Item(word, s, s, explicit || immediate)) Some(Completion.Result(word, cs.length == 1, items.sorted(history.ordering))) diff -r e2d71b8b0d95 -r bf4bbe72f740 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Wed Feb 19 21:38:44 2014 +0100 +++ b/src/Pure/PIDE/markup.ML Thu Feb 20 12:53:12 2014 +0100 @@ -20,7 +20,8 @@ val name: string -> T -> T val kindN: string val instanceN: string - val languageN: string val language: string -> T + val symbolsN: string + val languageN: string val language: string -> bool -> T val language_sort: T val language_type: T val language_term: T @@ -246,17 +247,19 @@ (* embedded languages *) -val (languageN, language) = markup_string "language" nameN; +val symbolsN = "symbols"; +val languageN = "language"; +fun language name symbols = (languageN, [(nameN, name), (symbolsN, print_bool symbols)]); -val language_sort = language "sort"; -val language_type = language "type"; -val language_term = language "term"; -val language_prop = language "prop"; +val language_sort = language "sort" true; +val language_type = language "type" true; +val language_term = language "term" true; +val language_prop = language "prop" true; -val language_ML = language "ML"; -val language_document = language "document"; -val language_text = language "text"; -val language_rail = language "rail"; +val language_ML = language "ML" false; +val language_document = language "document" false; +val language_text = language "text" true; +val language_rail = language "rail" true; (* formal entities *) diff -r e2d71b8b0d95 -r bf4bbe72f740 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Wed Feb 19 21:38:44 2014 +0100 +++ b/src/Pure/PIDE/markup.scala Thu Feb 20 12:53:12 2014 +0100 @@ -59,7 +59,7 @@ markup match { case Markup(ENTITY, props) => (props, props) match { - case (Kind(kind), Name(name)) => Some(kind, name) + case (Kind(kind), Name(name)) => Some((kind, name)) case _ => None } case _ => None @@ -87,8 +87,22 @@ /* embedded languages */ + val SYMBOLS = "symbols" + val Symbols = new Properties.Boolean(SYMBOLS) + val LANGUAGE = "language" - val Language = new Markup_String(LANGUAGE, NAME) + object Language + { + def unapply(markup: Markup): Option[(String, Boolean)] = + markup match { + case Markup(LANGUAGE, props) => + (props, props) match { + case (Name(name), Symbols(symbols)) => Some((name, symbols)) + case _ => None + } + case _ => None + } + } /* external resources */ diff -r e2d71b8b0d95 -r bf4bbe72f740 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Wed Feb 19 21:38:44 2014 +0100 +++ b/src/Tools/jEdit/src/completion_popup.scala Thu Feb 20 12:53:12 2014 +0100 @@ -110,7 +110,12 @@ val history = PIDE.completion_history.value val decode = Isabelle_Encoding.is_active(buffer) - syntax.completion.complete(history, decode, explicit, text) match { + val context = + PIDE.document_view(text_area) match { + case None => Completion.Context.default + case Some(doc_view) => doc_view.get_rendering().completion_context(caret) + } + syntax.completion.complete(history, decode, explicit, text, context) match { case Some(result) => if (result.unique && result.items.head.immediate && immediate) insert(result.items.head) @@ -277,7 +282,8 @@ val caret = text_field.getCaret.getDot val text = text_field.getText.substring(0, caret) - syntax.completion.complete(history, decode = true, explicit = false, text) match { + syntax.completion.complete( + history, decode = true, explicit = false, text, Completion.Context.default) match { case Some(result) => val fm = text_field.getFontMetrics(text_field.getFont) val loc = diff -r e2d71b8b0d95 -r bf4bbe72f740 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Wed Feb 19 21:38:44 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Thu Feb 20 12:53:12 2014 +0100 @@ -200,6 +200,31 @@ val dynamic_color = color_value("dynamic_color") + /* completion context */ + + private val completion_elements = + Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, + Markup.COMMENT, Markup.LANGUAGE) + + def completion_context(caret: Text.Offset): Completion.Context = + if (caret > 0) { + val result = + snapshot.select_markup(Text.Range(caret - 1, caret + 1), Some(completion_elements), _ => + { + case Text.Info(_, XML.Elem(Markup.Language(language, symbols), _)) => + Some(Completion.Context(language, symbols)) + case Text.Info(_, XML.Elem(markup, _)) => + if (completion_elements(markup.name)) Some(Completion.Context("unknown", true)) + else None + }) + result match { + case Text.Info(_, context) :: _ => context + case Nil => Completion.Context.default + } + } + else Completion.Context.default + + /* command overview */ val overview_limit = options.int("jedit_text_overview_limit") @@ -429,8 +454,8 @@ Some(add(prev, r, (true, pretty_typing("::", body)))) case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) => Some(add(prev, r, (false, pretty_typing("ML:", body)))) - case (prev, Text.Info(r, XML.Elem(Markup.Language(name), _))) => - Some(add(prev, r, (true, XML.Text("language: " + name)))) + case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _), _))) => + Some(add(prev, r, (true, XML.Text("language: " + language)))) case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) => if (tooltips.isDefinedAt(name)) Some(add(prev, r, (true, XML.Text(tooltips(name)))))