# HG changeset patch # User wenzelm # Date 1392899029 -3600 # Node ID 25a7a998852a32a25ffc185b18235a9f564762e0 # Parent bf4bbe72f740e4b935499477b5e3568d9bbf482d default completion context via outer syntax; no symbol completion for ML files; tuned; diff -r bf4bbe72f740 -r 25a7a998852a src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Thu Feb 20 12:53:12 2014 +0100 +++ b/src/Pure/Isar/outer_syntax.scala Thu Feb 20 13:23:49 2014 +0100 @@ -43,6 +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 has_tokens: Boolean = true) { override def toString: String = @@ -72,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, true) + new Outer_Syntax(keywords1, lexicon1, completion1, completion_context, true) } def + (name: String, kind: (String, List[String])): Outer_Syntax = @@ -120,15 +121,10 @@ /* token language */ - def no_tokens: Outer_Syntax = - { - require(keywords.isEmpty && lexicon.isEmpty) - new Outer_Syntax(completion = completion, has_tokens = false) - } - def scan(input: Reader[Char]): List[Token] = { - Token.Parsers.parseAll(Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), input) match { + Token.Parsers.parseAll( + Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), input) match { case Token.Parsers.Success(tokens, _) => tokens case _ => error("Unexpected failure of tokenizing input:\n" + input.source.toString) } @@ -151,4 +147,19 @@ } (toks.toList, ctxt) } + + + /* language context */ + + def set_completion_context(context: Completion.Context): Outer_Syntax = + new Outer_Syntax(keywords, lexicon, completion, context, has_tokens) + + def no_tokens: Outer_Syntax = + { + require(keywords.isEmpty && lexicon.isEmpty) + new Outer_Syntax( + completion = completion, + completion_context = completion_context, + has_tokens = false) + } } diff -r bf4bbe72f740 -r 25a7a998852a src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Thu Feb 20 12:53:12 2014 +0100 +++ b/src/Pure/PIDE/markup.scala Thu Feb 20 13:23:49 2014 +0100 @@ -93,6 +93,9 @@ val LANGUAGE = "language" object Language { + val ML = "ML" + val UNKNOWN = "unknown" + def unapply(markup: Markup): Option[(String, Boolean)] = markup match { case Markup(LANGUAGE, props) => diff -r bf4bbe72f740 -r 25a7a998852a src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Thu Feb 20 12:53:12 2014 +0100 +++ b/src/Tools/jEdit/src/completion_popup.scala Thu Feb 20 13:23:49 2014 +0100 @@ -111,10 +111,11 @@ val history = PIDE.completion_history.value val decode = Isabelle_Encoding.is_active(buffer) val context = - PIDE.document_view(text_area) match { - case None => Completion.Context.default + (PIDE.document_view(text_area) match { + case None => None case Some(doc_view) => doc_view.get_rendering().completion_context(caret) - } + }) getOrElse syntax.completion_context + syntax.completion.complete(history, decode, explicit, text, context) match { case Some(result) => if (result.unique && result.items.head.immediate && immediate) @@ -283,7 +284,7 @@ val text = text_field.getText.substring(0, caret) syntax.completion.complete( - history, decode = true, explicit = false, text, Completion.Context.default) match { + history, decode = true, explicit = false, text, syntax.completion_context) match { case Some(result) => val fm = text_field.getFontMetrics(text_field.getFont) val loc = diff -r bf4bbe72f740 -r 25a7a998852a src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Thu Feb 20 12:53:12 2014 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Thu Feb 20 13:23:49 2014 +0100 @@ -31,7 +31,12 @@ "isabelle-output", // pretty text area output "isabelle-root") // session ROOT - private lazy val symbols_syntax = Outer_Syntax.init().no_tokens + private lazy val ml_syntax: Outer_Syntax = + Outer_Syntax.init().no_tokens. + set_completion_context(Completion.Context(Markup.Language.ML, false)) + + private lazy val news_syntax: Outer_Syntax = + Outer_Syntax.init().no_tokens def mode_syntax(name: String): Option[Outer_Syntax] = name match { @@ -40,7 +45,8 @@ if (syntax == Outer_Syntax.empty) None else Some(syntax) case "isabelle-options" => Some(Options.options_syntax) case "isabelle-root" => Some(Build.root_syntax) - case "isabelle-ml" | "isabelle-news" => Some(symbols_syntax) + case "isabelle-ml" => Some(ml_syntax) + case "isabelle-news" => Some(news_syntax) case "isabelle-output" => None case _ => None } diff -r bf4bbe72f740 -r 25a7a998852a src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Thu Feb 20 12:53:12 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Thu Feb 20 13:23:49 2014 +0100 @@ -206,7 +206,7 @@ Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE) - def completion_context(caret: Text.Offset): Completion.Context = + def completion_context(caret: Text.Offset): Option[Completion.Context] = if (caret > 0) { val result = snapshot.select_markup(Text.Range(caret - 1, caret + 1), Some(completion_elements), _ => @@ -214,15 +214,16 @@ 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)) + if (completion_elements(markup.name)) + Some(Completion.Context(Markup.Language.UNKNOWN, true)) else None }) result match { - case Text.Info(_, context) :: _ => context - case Nil => Completion.Context.default + case Text.Info(_, context) :: _ => Some(context) + case Nil => None } } - else Completion.Context.default + else None /* command overview */