default completion context via outer syntax;
authorwenzelm
Thu Feb 20 13:23:49 2014 +0100 (2014-02-20 ago)
changeset 5561625a7a998852a
parent 55615 bf4bbe72f740
child 55617 2c585bb9560c
default completion context via outer syntax;
no symbol completion for ML files;
tuned;
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/markup.scala
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Thu Feb 20 12:53:12 2014 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Feb 20 13:23:49 2014 +0100
     1.3 @@ -43,6 +43,7 @@
     1.4    keywords: Map[String, (String, List[String])] = Map.empty,
     1.5    lexicon: Scan.Lexicon = Scan.Lexicon.empty,
     1.6    val completion: Completion = Completion.empty,
     1.7 +  val completion_context: Completion.Context = Completion.Context.default,
     1.8    val has_tokens: Boolean = true)
     1.9  {
    1.10    override def toString: String =
    1.11 @@ -72,7 +73,7 @@
    1.12      val completion1 =
    1.13        if (Keyword.control(kind._1) || replace == Some("")) completion
    1.14        else completion + (name, replace getOrElse name)
    1.15 -    new Outer_Syntax(keywords1, lexicon1, completion1, true)
    1.16 +    new Outer_Syntax(keywords1, lexicon1, completion1, completion_context, true)
    1.17    }
    1.18  
    1.19    def + (name: String, kind: (String, List[String])): Outer_Syntax =
    1.20 @@ -120,15 +121,10 @@
    1.21  
    1.22    /* token language */
    1.23  
    1.24 -  def no_tokens: Outer_Syntax =
    1.25 -  {
    1.26 -    require(keywords.isEmpty && lexicon.isEmpty)
    1.27 -    new Outer_Syntax(completion = completion, has_tokens = false)
    1.28 -  }
    1.29 -
    1.30    def scan(input: Reader[Char]): List[Token] =
    1.31    {
    1.32 -    Token.Parsers.parseAll(Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), input) match {
    1.33 +    Token.Parsers.parseAll(
    1.34 +        Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), input) match {
    1.35        case Token.Parsers.Success(tokens, _) => tokens
    1.36        case _ => error("Unexpected failure of tokenizing input:\n" + input.source.toString)
    1.37      }
    1.38 @@ -151,4 +147,19 @@
    1.39      }
    1.40      (toks.toList, ctxt)
    1.41    }
    1.42 +
    1.43 +
    1.44 +  /* language context */
    1.45 +
    1.46 +  def set_completion_context(context: Completion.Context): Outer_Syntax =
    1.47 +    new Outer_Syntax(keywords, lexicon, completion, context, has_tokens)
    1.48 +
    1.49 +  def no_tokens: Outer_Syntax =
    1.50 +  {
    1.51 +    require(keywords.isEmpty && lexicon.isEmpty)
    1.52 +    new Outer_Syntax(
    1.53 +      completion = completion,
    1.54 +      completion_context = completion_context,
    1.55 +      has_tokens = false)
    1.56 +  }
    1.57  }
     2.1 --- a/src/Pure/PIDE/markup.scala	Thu Feb 20 12:53:12 2014 +0100
     2.2 +++ b/src/Pure/PIDE/markup.scala	Thu Feb 20 13:23:49 2014 +0100
     2.3 @@ -93,6 +93,9 @@
     2.4    val LANGUAGE = "language"
     2.5    object Language
     2.6    {
     2.7 +    val ML = "ML"
     2.8 +    val UNKNOWN = "unknown"
     2.9 +
    2.10      def unapply(markup: Markup): Option[(String, Boolean)] =
    2.11        markup match {
    2.12          case Markup(LANGUAGE, props) =>
     3.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Feb 20 12:53:12 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Feb 20 13:23:49 2014 +0100
     3.3 @@ -111,10 +111,11 @@
     3.4              val history = PIDE.completion_history.value
     3.5              val decode = Isabelle_Encoding.is_active(buffer)
     3.6              val context =
     3.7 -              PIDE.document_view(text_area) match {
     3.8 -                case None => Completion.Context.default
     3.9 +              (PIDE.document_view(text_area) match {
    3.10 +                case None => None
    3.11                  case Some(doc_view) => doc_view.get_rendering().completion_context(caret)
    3.12 -              }
    3.13 +              }) getOrElse syntax.completion_context
    3.14 +
    3.15              syntax.completion.complete(history, decode, explicit, text, context) match {
    3.16                case Some(result) =>
    3.17                  if (result.unique && result.items.head.immediate && immediate)
    3.18 @@ -283,7 +284,7 @@
    3.19            val text = text_field.getText.substring(0, caret)
    3.20  
    3.21            syntax.completion.complete(
    3.22 -              history, decode = true, explicit = false, text, Completion.Context.default) match {
    3.23 +              history, decode = true, explicit = false, text, syntax.completion_context) match {
    3.24              case Some(result) =>
    3.25                val fm = text_field.getFontMetrics(text_field.getFont)
    3.26                val loc =
     4.1 --- a/src/Tools/jEdit/src/isabelle.scala	Thu Feb 20 12:53:12 2014 +0100
     4.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Thu Feb 20 13:23:49 2014 +0100
     4.3 @@ -31,7 +31,12 @@
     4.4        "isabelle-output",  // pretty text area output
     4.5        "isabelle-root")    // session ROOT
     4.6  
     4.7 -  private lazy val symbols_syntax = Outer_Syntax.init().no_tokens
     4.8 +  private lazy val ml_syntax: Outer_Syntax =
     4.9 +    Outer_Syntax.init().no_tokens.
    4.10 +      set_completion_context(Completion.Context(Markup.Language.ML, false))
    4.11 +
    4.12 +  private lazy val news_syntax: Outer_Syntax =
    4.13 +    Outer_Syntax.init().no_tokens
    4.14  
    4.15    def mode_syntax(name: String): Option[Outer_Syntax] =
    4.16      name match {
    4.17 @@ -40,7 +45,8 @@
    4.18          if (syntax == Outer_Syntax.empty) None else Some(syntax)
    4.19        case "isabelle-options" => Some(Options.options_syntax)
    4.20        case "isabelle-root" => Some(Build.root_syntax)
    4.21 -      case "isabelle-ml" | "isabelle-news" => Some(symbols_syntax)
    4.22 +      case "isabelle-ml" => Some(ml_syntax)
    4.23 +      case "isabelle-news" => Some(news_syntax)
    4.24        case "isabelle-output" => None
    4.25        case _ => None
    4.26      }
     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 12:53:12 2014 +0100
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 13:23:49 2014 +0100
     5.3 @@ -206,7 +206,7 @@
     5.4      Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE,
     5.5        Markup.COMMENT, Markup.LANGUAGE)
     5.6  
     5.7 -  def completion_context(caret: Text.Offset): Completion.Context =
     5.8 +  def completion_context(caret: Text.Offset): Option[Completion.Context] =
     5.9      if (caret > 0) {
    5.10        val result =
    5.11          snapshot.select_markup(Text.Range(caret - 1, caret + 1), Some(completion_elements), _ =>
    5.12 @@ -214,15 +214,16 @@
    5.13              case Text.Info(_, XML.Elem(Markup.Language(language, symbols), _)) =>
    5.14                Some(Completion.Context(language, symbols))
    5.15              case Text.Info(_, XML.Elem(markup, _)) =>
    5.16 -              if (completion_elements(markup.name)) Some(Completion.Context("unknown", true))
    5.17 +              if (completion_elements(markup.name))
    5.18 +                Some(Completion.Context(Markup.Language.UNKNOWN, true))
    5.19                else None
    5.20            })
    5.21        result match {
    5.22 -        case Text.Info(_, context) :: _ => context
    5.23 -        case Nil => Completion.Context.default
    5.24 +        case Text.Info(_, context) :: _ => Some(context)
    5.25 +        case Nil => None
    5.26        }
    5.27      }
    5.28 -    else Completion.Context.default
    5.29 +    else None
    5.30  
    5.31  
    5.32    /* command overview */