refined language context: antiquotes;
support default completions, with move of caret position;
tuned signature;
--- a/src/Pure/Isar/completion.scala Fri Feb 21 23:42:43 2014 +0100
+++ b/src/Pure/Isar/completion.scala Sat Feb 22 15:07:33 2014 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/Isar/completion.scala
Author: Makarius
-Completion of symbols and keywords.
+Completion of keywords and symbols, with abbreviations.
*/
package isabelle
@@ -18,10 +18,13 @@
object Context
{
- val default = Context("", true)
+ val outer = Context("", true, false)
+ val inner = Context(Markup.Language.UNKNOWN, true, false)
+ val ML_outer = Context(Markup.Language.ML, false, false)
+ val ML_inner = Context(Markup.Language.ML, true, true)
}
- sealed case class Context(language: String, symbols: Boolean)
+ sealed case class Context(language: String, symbols: Boolean, antiquotes: Boolean)
{
def is_outer: Boolean = language == ""
}
@@ -31,10 +34,11 @@
sealed case class Item(
original: String,
+ name: String,
replacement: String,
- description: String,
+ move: Int,
immediate: Boolean)
- { override def toString: String = description }
+ { override def toString: String = name }
sealed case class Result(original: String, unique: Boolean, items: List[Item])
@@ -92,8 +96,8 @@
new Ordering[Item] {
def compare(item1: Item, item2: Item): Int =
{
- frequency(item1.replacement) compare frequency(item2.replacement) match {
- case 0 => item1.replacement compare item2.replacement
+ frequency(item1.name) compare frequency(item2.name) match {
+ case 0 => item1.name compare item2.name
case ord => - ord
}
}
@@ -122,7 +126,7 @@
}
def update(item: Item, freq: Int = 1): Unit = synchronized {
- history = history + (item.replacement -> freq)
+ history = history + (item.name -> freq)
}
}
@@ -154,6 +158,14 @@
}
}
}
+
+
+ /* abbreviations */
+
+ private val caret = '\007'
+ private val antiquote = "@{"
+ private val default_abbrs =
+ Map("@{" -> "@{\007}", "`" -> "\\<open>\007\\<close>")
}
final class Completion private(
@@ -182,9 +194,13 @@
(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 =
+ val symbol_abbrs =
(for ((x, y) <- Symbol.abbrevs.iterator if !Completion.Word_Parsers.is_word(y))
- yield (y.reverse, (y, x))).toList
+ yield (y, x)).toList
+
+ val abbrs =
+ for ((a, b) <- symbol_abbrs ::: Completion.default_abbrs.toList)
+ yield (a.reverse, (a, b))
new Completion(
keywords,
@@ -205,17 +221,19 @@
context: Completion.Context): Option[Completion.Result] =
{
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
+ 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, _) :: _ =>
+ val ok =
+ if (a == Completion.antiquote) context.antiquotes
+ else context.symbols || Completion.default_abbrs.isDefinedAt(a)
+ if (ok) Some((a, abbrevs.map(_._2))) else None
+ }
+ case _ => None
+ }
val words_result =
abbrevs_result orElse {
@@ -241,7 +259,15 @@
val immediate =
!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))
+ val items =
+ ds.map(s => {
+ val (s1, s2) =
+ space_explode(Completion.caret, s) match {
+ case List(s1, s2) => (s1, s2)
+ case _ => (s, "")
+ }
+ Completion.Item(word, s, s1 + s2, - s2.length, explicit || immediate)
+ })
Some(Completion.Result(word, cs.length == 1, items.sorted(history.ordering)))
}
case None => None
--- a/src/Pure/Isar/outer_syntax.scala Fri Feb 21 23:42:43 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Sat Feb 22 15:07:33 2014 +0100
@@ -43,7 +43,7 @@
keywords: Map[String, (String, List[String])] = Map.empty,
lexicon: Scan.Lexicon = Scan.Lexicon.empty,
val completion: Completion = Completion.empty,
- val completion_context: Completion.Context = Completion.Context.default,
+ val completion_context: Completion.Context = Completion.Context.outer,
val has_tokens: Boolean = true)
{
override def toString: String =
--- a/src/Pure/PIDE/markup.ML Fri Feb 21 23:42:43 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Sat Feb 22 15:07:33 2014 +0100
@@ -21,7 +21,8 @@
val kindN: string
val instanceN: string
val symbolsN: string
- val languageN: string val language: string -> bool -> T
+ val languageN: string
+ val language: {name: string, symbols: bool, antiquotes: bool} -> T
val language_sort: T
val language_type: T
val language_term: T
@@ -249,18 +250,22 @@
(* embedded languages *)
val symbolsN = "symbols";
+val antiquotesN = "antiquotes";
val languageN = "language";
-fun language name symbols = (languageN, [(nameN, name), (symbolsN, print_bool symbols)]);
+
+fun language {name, symbols, antiquotes} =
+ (languageN,
+ [(nameN, name), (symbolsN, print_bool symbols), (antiquotesN, print_bool antiquotes)]);
-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" false;
-val language_document = language "document" false;
-val language_antiquotation = language "antiquotation" true;
-val language_text = language "text" true;
-val language_rail = language "rail" true;
+val language_sort = language {name = "sort", symbols = true, antiquotes = false};
+val language_type = language {name = "type", symbols = true, antiquotes = false};
+val language_term = language {name = "term", symbols = true, antiquotes = false};
+val language_prop = language {name = "prop", symbols = true, antiquotes = false};
+val language_ML = language {name = "ML", symbols = false, antiquotes = true};
+val language_document = language {name = "document", symbols = false, antiquotes = true};
+val language_antiquotation = language {name = "antiquotation", symbols = true, antiquotes = false};
+val language_text = language {name = "text", symbols = true, antiquotes = false};
+val language_rail = language {name = "rail", symbols = true, antiquotes = true};
(* formal entities *)
--- a/src/Pure/PIDE/markup.scala Fri Feb 21 23:42:43 2014 +0100
+++ b/src/Pure/PIDE/markup.scala Sat Feb 22 15:07:33 2014 +0100
@@ -87,8 +87,8 @@
/* embedded languages */
- val SYMBOLS = "symbols"
- val Symbols = new Properties.Boolean(SYMBOLS)
+ val Symbols = new Properties.Boolean("symbols")
+ val Antiquotes = new Properties.Boolean("antiquotes")
val LANGUAGE = "language"
object Language
@@ -96,11 +96,12 @@
val ML = "ML"
val UNKNOWN = "unknown"
- def unapply(markup: Markup): Option[(String, Boolean)] =
+ def unapply(markup: Markup): Option[(String, Boolean, Boolean)] =
markup match {
case Markup(LANGUAGE, props) =>
- (props, props) match {
- case (Name(name), Symbols(symbols)) => Some((name, symbols))
+ (props, props, props) match {
+ case (Name(name), Symbols(symbols), Antiquotes(antiquotes)) =>
+ Some((name, symbols, antiquotes))
case _ => None
}
case _ => None
--- a/src/Tools/jEdit/src/completion_popup.scala Fri Feb 21 23:42:43 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Sat Feb 22 15:07:33 2014 +0100
@@ -87,6 +87,8 @@
case Some(text) if text == item.original =>
buffer.remove(caret - len, len)
buffer.insert(caret - len, item.replacement)
+ if (item.move != 0)
+ text_area.moveCaretPosition(text_area.getCaretPosition + item.move)
case _ =>
}
}
@@ -265,7 +267,7 @@
content.substring(0, caret - len) +
item.replacement +
content.substring(caret))
- text_field.getCaret.setDot(caret - len + item.replacement.length)
+ text_field.getCaret.setDot(caret - len + item.replacement.length + item.move)
case _ =>
}
}
--- a/src/Tools/jEdit/src/isabelle.scala Fri Feb 21 23:42:43 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Sat Feb 22 15:07:33 2014 +0100
@@ -33,7 +33,7 @@
private lazy val ml_syntax: Outer_Syntax =
Outer_Syntax.init().no_tokens.
- set_completion_context(Completion.Context(Markup.Language.ML, false))
+ set_completion_context(Completion.Context.ML_outer)
private lazy val news_syntax: Outer_Syntax =
Outer_Syntax.init().no_tokens
--- a/src/Tools/jEdit/src/rendering.scala Fri Feb 21 23:42:43 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Sat Feb 22 15:07:33 2014 +0100
@@ -278,11 +278,11 @@
{
case Text.Info(_, elem)
if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
- Some(Completion.Context(Markup.Language.ML, true))
- case Text.Info(_, XML.Elem(Markup.Language(language, symbols), _)) =>
- Some(Completion.Context(language, symbols))
- case Text.Info(_, XML.Elem(markup, _)) =>
- Some(Completion.Context(Markup.Language.UNKNOWN, true))
+ Some(Completion.Context.ML_inner)
+ case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) =>
+ Some(Completion.Context(language, symbols, antiquotes))
+ case Text.Info(_, _) =>
+ Some(Completion.Context.inner)
})
result match {
case Text.Info(_, context) :: _ => Some(context)
@@ -500,7 +500,7 @@
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(language, _), _))) =>
+ 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, _), _))) =>
Rendering.tooltip_descriptions.get(name).