# HG changeset patch # User wenzelm # Date 1393358277 -3600 # Node ID 75a48dc4383e1e0c5a61a42f96fc9c96c44d13d6 # Parent 2e1398b484aa994992016b1ec2ac317750dc24ff tuned signature; diff -r 2e1398b484aa -r 75a48dc4383e src/Pure/General/completion.scala --- 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 diff -r 2e1398b484aa -r 75a48dc4383e src/Pure/Isar/outer_syntax.scala --- 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) } } diff -r 2e1398b484aa -r 75a48dc4383e src/Tools/jEdit/src/completion_popup.scala --- 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) => diff -r 2e1398b484aa -r 75a48dc4383e src/Tools/jEdit/src/isabelle.scala --- 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 diff -r 2e1398b484aa -r 75a48dc4383e src/Tools/jEdit/src/rendering.scala --- 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)