--- 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)))
--- 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 *)
--- 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 */
--- 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 =
--- 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)))))