src/Tools/jEdit/src/rendering.scala
changeset 55501 fdde1d62e1fb
parent 55500 cdbbaa3074a8
child 55503 750206d988ee
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Feb 15 16:27:58 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Feb 15 16:49:10 2014 +0100
     1.3 @@ -67,7 +67,7 @@
     1.4    def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8
     1.5  
     1.6  
     1.7 -  /* token markup -- text styles */
     1.8 +  /* Isabelle/Isar token markup */
     1.9  
    1.10    private val command_style: Map[String, Byte] =
    1.11    {
    1.12 @@ -111,11 +111,20 @@
    1.13      else if (token.is_operator) JEditToken.OPERATOR
    1.14      else token_style(token.kind)
    1.15  
    1.16 +
    1.17 +  /* Isabelle/ML token markup */
    1.18 +
    1.19 +  private val ml_keyword2: Set[String] =
    1.20 +    Set("case", "do", "else", "end", "if", "in", "let", "local", "of",
    1.21 +      "sig", "struct", "then", "while", "with")
    1.22 +
    1.23 +  private val ml_keyword3: Set[String] =
    1.24 +    Set("handle", "open", "raise")
    1.25 +
    1.26    private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] =
    1.27    {
    1.28      import JEditToken._
    1.29      Map[ML_Lex.Kind.Value, Byte](
    1.30 -      ML_Lex.Kind.KEYWORD -> KEYWORD1,
    1.31        ML_Lex.Kind.IDENT -> NULL,
    1.32        ML_Lex.Kind.LONG_IDENT -> NULL,
    1.33        ML_Lex.Kind.TYPE_VAR -> NULL,
    1.34 @@ -131,8 +140,11 @@
    1.35    }
    1.36  
    1.37    def ml_token_markup(token: ML_Lex.Token): Byte =
    1.38 -    if (token.is_operator) JEditToken.OPERATOR
    1.39 -    else ml_token_style(token.kind)
    1.40 +    if (!token.is_keyword) ml_token_style(token.kind)
    1.41 +    else if (token.is_operator) JEditToken.OPERATOR
    1.42 +    else if (ml_keyword2(token.source)) JEditToken.KEYWORD2
    1.43 +    else if (ml_keyword3(token.source)) JEditToken.KEYWORD3
    1.44 +    else JEditToken.KEYWORD1
    1.45  }
    1.46  
    1.47