src/Tools/jEdit/src/rendering.scala
changeset 55505 2a1ca7f6607b
parent 55503 750206d988ee
child 55512 75c68e05f9ea
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Feb 15 17:10:57 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Feb 15 18:28:18 2014 +0100
     1.3 @@ -108,23 +108,17 @@
     1.4  
     1.5    def token_markup(syntax: Outer_Syntax, token: Token): Byte =
     1.6      if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
     1.7 -    else if (token.is_operator) JEditToken.OPERATOR
     1.8 +    else if (token.is_delimiter) JEditToken.OPERATOR
     1.9      else token_style(token.kind)
    1.10  
    1.11  
    1.12    /* Isabelle/ML token markup */
    1.13  
    1.14 -  private val ml_keyword2: Set[String] =
    1.15 -    Set("case", "do", "else", "end", "if", "in", "let", "local", "of",
    1.16 -      "sig", "struct", "then", "while", "with")
    1.17 -
    1.18 -  private val ml_keyword3: Set[String] =
    1.19 -    Set("handle", "open", "raise")
    1.20 -
    1.21    private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] =
    1.22    {
    1.23      import JEditToken._
    1.24      Map[ML_Lex.Kind.Value, Byte](
    1.25 +      ML_Lex.Kind.KEYWORD -> NULL,
    1.26        ML_Lex.Kind.IDENT -> NULL,
    1.27        ML_Lex.Kind.LONG_IDENT -> NULL,
    1.28        ML_Lex.Kind.TYPE_VAR -> NULL,
    1.29 @@ -141,9 +135,9 @@
    1.30  
    1.31    def ml_token_markup(token: ML_Lex.Token): Byte =
    1.32      if (!token.is_keyword) ml_token_style(token.kind)
    1.33 -    else if (token.is_operator) JEditToken.OPERATOR
    1.34 -    else if (ml_keyword2(token.source)) JEditToken.KEYWORD2
    1.35 -    else if (ml_keyword3(token.source)) JEditToken.KEYWORD3
    1.36 +    else if (token.is_delimiter) JEditToken.OPERATOR
    1.37 +    else if (ML_Lex.keywords2(token.source)) JEditToken.KEYWORD2
    1.38 +    else if (ML_Lex.keywords3(token.source)) JEditToken.KEYWORD3
    1.39      else JEditToken.KEYWORD1
    1.40  }
    1.41  
    1.42 @@ -183,6 +177,7 @@
    1.43    val active_result_color = color_value("active_result_color")
    1.44    val keyword1_color = color_value("keyword1_color")
    1.45    val keyword2_color = color_value("keyword2_color")
    1.46 +  val keyword3_color = color_value("keyword3_color")
    1.47  
    1.48    val tfree_color = color_value("tfree_color")
    1.49    val tvar_color = color_value("tvar_color")
    1.50 @@ -634,7 +629,9 @@
    1.51        Markup.INNER_CARTOUCHE -> inner_cartouche_color,
    1.52        Markup.INNER_COMMENT -> inner_comment_color,
    1.53        Markup.DYNAMIC_FACT -> dynamic_color,
    1.54 -      Markup.ML_KEYWORD -> keyword1_color,
    1.55 +      Markup.ML_KEYWORD1 -> keyword1_color,
    1.56 +      Markup.ML_KEYWORD2 -> keyword2_color,
    1.57 +      Markup.ML_KEYWORD3 -> keyword3_color,
    1.58        Markup.ML_DELIMITER -> Color.BLACK,
    1.59        Markup.ML_NUMERAL -> inner_numeral_color,
    1.60        Markup.ML_CHAR -> inner_quoted_color,