--- a/src/Pure/General/completion.scala Tue Feb 25 20:46:09 2014 +0100
+++ b/src/Pure/General/completion.scala Tue Feb 25 20:57:57 2014 +0100
@@ -166,15 +166,15 @@
/* language context */
- object Context
+ object Language_Context
{
- val outer = Context("", true, false)
- val inner = Context(Markup.Language.UNKNOWN, true, false)
- val ML_outer = Context(Markup.Language.ML, false, true)
- val ML_inner = Context(Markup.Language.ML, true, false)
+ val outer = Language_Context("", true, false)
+ val inner = Language_Context(Markup.Language.UNKNOWN, true, false)
+ val ML_outer = Language_Context(Markup.Language.ML, false, true)
+ val ML_inner = Language_Context(Markup.Language.ML, true, false)
}
- sealed case class Context(language: String, symbols: Boolean, antiquotes: Boolean)
+ sealed case class Language_Context(language: String, symbols: Boolean, antiquotes: Boolean)
{
def is_outer: Boolean = language == ""
}
@@ -281,7 +281,7 @@
text_start: Text.Offset,
text: CharSequence,
word_context: Boolean,
- context: Completion.Context): Option[Completion.Result] =
+ language_context: Completion.Language_Context): Option[Completion.Result] =
{
val abbrevs_result =
Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), new Library.Reverse(text)) match {
@@ -291,8 +291,8 @@
case Nil => None
case (a, _) :: _ =>
val ok =
- if (a == Completion.antiquote) context.antiquotes
- else context.symbols || Completion.default_abbrs.isDefinedAt(a)
+ if (a == Completion.antiquote) language_context.antiquotes
+ else language_context.symbols || Completion.default_abbrs.isDefinedAt(a)
if (ok) Some((a, abbrevs.map(_._2))) else None
}
case _ => None
@@ -307,7 +307,7 @@
val completions =
for {
s <- words_lex.completions(word)
- if (if (keywords(s)) context.is_outer else context.symbols)
+ if (if (keywords(s)) language_context.is_outer else language_context.symbols)
r <- words_map.get_list(s)
} yield r
if (completions.isEmpty) None
--- a/src/Pure/Isar/outer_syntax.scala Tue Feb 25 20:46:09 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Tue Feb 25 20:57:57 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.outer,
+ val language_context: Completion.Language_Context = Completion.Language_Context.outer,
val has_tokens: Boolean = true)
{
override def toString: String =
@@ -73,7 +73,7 @@
val completion1 =
if (Keyword.control(kind._1) || replace == Some("")) completion
else completion + (name, replace getOrElse name)
- new Outer_Syntax(keywords1, lexicon1, completion1, completion_context, true)
+ new Outer_Syntax(keywords1, lexicon1, completion1, language_context, true)
}
def + (name: String, kind: (String, List[String])): Outer_Syntax =
@@ -151,7 +151,7 @@
/* language context */
- def set_completion_context(context: Completion.Context): Outer_Syntax =
+ def set_language_context(context: Completion.Language_Context): Outer_Syntax =
new Outer_Syntax(keywords, lexicon, completion, context, has_tokens)
def no_tokens: Outer_Syntax =
@@ -159,7 +159,7 @@
require(keywords.isEmpty && lexicon.isEmpty)
new Outer_Syntax(
completion = completion,
- completion_context = completion_context,
+ language_context = language_context,
has_tokens = false)
}
}
--- a/src/Tools/jEdit/src/completion_popup.scala Tue Feb 25 20:46:09 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Tue Feb 25 20:57:57 2014 +0100
@@ -144,9 +144,9 @@
val context =
(opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
case Some(rendering) =>
- rendering.completion_context(JEdit_Lib.stretch_point_range(buffer, caret))
+ rendering.language_context(JEdit_Lib.stretch_point_range(buffer, caret))
case None => None
- }) getOrElse syntax.completion_context
+ }) getOrElse syntax.language_context
syntax.completion.complete(history, decode, explicit, start, text, word_context, context)
@@ -392,7 +392,7 @@
Completion.word_context(JEdit_Lib.try_get_text(text_field.getText,
Text.Range(caret, caret + 1))) // FIXME proper point range!?
- val context = syntax.completion_context
+ val context = syntax.language_context
syntax.completion.complete(history, true, false, 0, text, word_context, context) match {
case Some(result) =>
--- a/src/Tools/jEdit/src/isabelle.scala Tue Feb 25 20:46:09 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Tue Feb 25 20:57:57 2014 +0100
@@ -33,7 +33,7 @@
private lazy val ml_syntax: Outer_Syntax =
Outer_Syntax.init().no_tokens.
- set_completion_context(Completion.Context.ML_outer)
+ set_language_context(Completion.Language_Context.ML_outer)
private lazy val news_syntax: Outer_Syntax =
Outer_Syntax.init().no_tokens
--- a/src/Tools/jEdit/src/rendering.scala Tue Feb 25 20:46:09 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Tue Feb 25 20:57:57 2014 +0100
@@ -152,7 +152,7 @@
private val completion_names_elements = Set(Markup.COMPLETION)
- private val completion_context_elements =
+ private val language_context_elements =
Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
Markup.ML_STRING, Markup.ML_COMMENT)
@@ -288,16 +288,16 @@
}).headOption.map(_.info)
}
- def completion_context(range: Text.Range): Option[Completion.Context] =
- snapshot.select(range, Rendering.completion_context_elements, _ =>
+ def language_context(range: Text.Range): Option[Completion.Language_Context] =
+ snapshot.select(range, Rendering.language_context_elements, _ =>
{
case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) =>
- Some(Completion.Context(language, symbols, antiquotes))
+ Some(Completion.Language_Context(language, symbols, antiquotes))
case Text.Info(_, elem)
if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
- Some(Completion.Context.ML_inner)
+ Some(Completion.Language_Context.ML_inner)
case Text.Info(_, _) =>
- Some(Completion.Context.inner)
+ Some(Completion.Language_Context.inner)
}).headOption.map(_.info)