# HG changeset patch
# User wenzelm
# Date 1308390307 -7200
# Node ID 1ed88ddf1268f72e94a3a1b01105519377dc2663
# Parent  095f90f8dca3decdcec03825bb8c6c03c221e852
more uniform treatment of "keyword" vs. "operator";

diff -r 095f90f8dca3 -r 1ed88ddf1268 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Sat Jun 18 11:22:03 2011 +0200
+++ b/src/Pure/Isar/token.scala	Sat Jun 18 11:45:07 2011 +0200
@@ -64,7 +64,7 @@
 sealed case class Token(val kind: Token.Kind.Value, val source: String)
 {
   def is_command: Boolean = kind == Token.Kind.COMMAND
-  def is_keyword: Boolean = kind == Token.Kind.KEYWORD
+  def is_operator: Boolean = kind == Token.Kind.KEYWORD && !Symbol.is_ascii_identifier(source)
   def is_delimited: Boolean =
     kind == Token.Kind.STRING ||
     kind == Token.Kind.ALT_STRING ||
diff -r 095f90f8dca3 -r 1ed88ddf1268 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Sat Jun 18 11:22:03 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Sat Jun 18 11:45:07 2011 +0200
@@ -65,7 +65,7 @@
   | Token.EOF           => Markup.control;
 
 fun token_markup tok =
-  if Token.keyword_with (not o Lexicon.is_identifier) tok then Markup.operator
+  if Token.keyword_with (not o Lexicon.is_ascii_identifier) tok then Markup.operator
   else
     let
       val kind = Token.kind_of tok;
diff -r 095f90f8dca3 -r 1ed88ddf1268 src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Jun 18 11:22:03 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Jun 18 11:45:07 2011 +0200
@@ -213,9 +213,7 @@
   }
 
   def token_markup(syntax: Outer_Syntax, token: Token): Byte =
-    if (token.is_command)
-      command_style(syntax.keyword_kind(token.content).getOrElse(""))
-    else if (token.is_keyword && !Symbol.is_ascii_identifier(token.content))
-      JEditToken.OPERATOR
+    if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
+    else if (token.is_operator) JEditToken.OPERATOR
     else token_style(token.kind)
 }