# HG changeset patch # User wenzelm # Date 1392479350 -3600 # Node ID fdde1d62e1fb6805fd89314097cad0a37cc880bd # Parent cdbbaa3074a8d408db9683159cc99537beb70205 refined ML keyword styles; diff -r cdbbaa3074a8 -r fdde1d62e1fb src/Pure/ML/ml_lex.scala --- a/src/Pure/ML/ml_lex.scala Sat Feb 15 16:27:58 2014 +0100 +++ b/src/Pure/ML/ml_lex.scala Sat Feb 15 16:49:10 2014 +0100 @@ -33,7 +33,8 @@ sealed case class Token(val kind: Kind.Value, val source: String) { - def is_operator: Boolean = kind == Kind.KEYWORD && !Symbol.is_ascii_identifier(source) + def is_keyword: Boolean = kind == Kind.KEYWORD + def is_operator: Boolean = is_keyword && !Symbol.is_ascii_identifier(source) } diff -r cdbbaa3074a8 -r fdde1d62e1fb src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Sat Feb 15 16:27:58 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Sat Feb 15 16:49:10 2014 +0100 @@ -67,7 +67,7 @@ def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8 - /* token markup -- text styles */ + /* Isabelle/Isar token markup */ private val command_style: Map[String, Byte] = { @@ -111,11 +111,20 @@ else if (token.is_operator) JEditToken.OPERATOR else token_style(token.kind) + + /* Isabelle/ML token markup */ + + private val ml_keyword2: Set[String] = + Set("case", "do", "else", "end", "if", "in", "let", "local", "of", + "sig", "struct", "then", "while", "with") + + private val ml_keyword3: Set[String] = + Set("handle", "open", "raise") + private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] = { import JEditToken._ Map[ML_Lex.Kind.Value, Byte]( - ML_Lex.Kind.KEYWORD -> KEYWORD1, ML_Lex.Kind.IDENT -> NULL, ML_Lex.Kind.LONG_IDENT -> NULL, ML_Lex.Kind.TYPE_VAR -> NULL, @@ -131,8 +140,11 @@ } def ml_token_markup(token: ML_Lex.Token): Byte = - if (token.is_operator) JEditToken.OPERATOR - else ml_token_style(token.kind) + if (!token.is_keyword) ml_token_style(token.kind) + else if (token.is_operator) JEditToken.OPERATOR + else if (ml_keyword2(token.source)) JEditToken.KEYWORD2 + else if (ml_keyword3(token.source)) JEditToken.KEYWORD3 + else JEditToken.KEYWORD1 }