refined ML keyword styles;
authorwenzelm
Sat Feb 15 16:49:10 2014 +0100 (2014-02-15 ago)
changeset 55501fdde1d62e1fb
parent 55500 cdbbaa3074a8
child 55502 72238ea2201c
refined ML keyword styles;
src/Pure/ML/ml_lex.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/ML/ml_lex.scala	Sat Feb 15 16:27:58 2014 +0100
     1.2 +++ b/src/Pure/ML/ml_lex.scala	Sat Feb 15 16:49:10 2014 +0100
     1.3 @@ -33,7 +33,8 @@
     1.4  
     1.5    sealed case class Token(val kind: Kind.Value, val source: String)
     1.6    {
     1.7 -    def is_operator: Boolean = kind == Kind.KEYWORD && !Symbol.is_ascii_identifier(source)
     1.8 +    def is_keyword: Boolean = kind == Kind.KEYWORD
     1.9 +    def is_operator: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
    1.10    }
    1.11  
    1.12  
     2.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Feb 15 16:27:58 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Feb 15 16:49:10 2014 +0100
     2.3 @@ -67,7 +67,7 @@
     2.4    def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8
     2.5  
     2.6  
     2.7 -  /* token markup -- text styles */
     2.8 +  /* Isabelle/Isar token markup */
     2.9  
    2.10    private val command_style: Map[String, Byte] =
    2.11    {
    2.12 @@ -111,11 +111,20 @@
    2.13      else if (token.is_operator) JEditToken.OPERATOR
    2.14      else token_style(token.kind)
    2.15  
    2.16 +
    2.17 +  /* Isabelle/ML token markup */
    2.18 +
    2.19 +  private val ml_keyword2: Set[String] =
    2.20 +    Set("case", "do", "else", "end", "if", "in", "let", "local", "of",
    2.21 +      "sig", "struct", "then", "while", "with")
    2.22 +
    2.23 +  private val ml_keyword3: Set[String] =
    2.24 +    Set("handle", "open", "raise")
    2.25 +
    2.26    private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] =
    2.27    {
    2.28      import JEditToken._
    2.29      Map[ML_Lex.Kind.Value, Byte](
    2.30 -      ML_Lex.Kind.KEYWORD -> KEYWORD1,
    2.31        ML_Lex.Kind.IDENT -> NULL,
    2.32        ML_Lex.Kind.LONG_IDENT -> NULL,
    2.33        ML_Lex.Kind.TYPE_VAR -> NULL,
    2.34 @@ -131,8 +140,11 @@
    2.35    }
    2.36  
    2.37    def ml_token_markup(token: ML_Lex.Token): Byte =
    2.38 -    if (token.is_operator) JEditToken.OPERATOR
    2.39 -    else ml_token_style(token.kind)
    2.40 +    if (!token.is_keyword) ml_token_style(token.kind)
    2.41 +    else if (token.is_operator) JEditToken.OPERATOR
    2.42 +    else if (ml_keyword2(token.source)) JEditToken.KEYWORD2
    2.43 +    else if (ml_keyword3(token.source)) JEditToken.KEYWORD3
    2.44 +    else JEditToken.KEYWORD1
    2.45  }
    2.46  
    2.47