# 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
 }