# HG changeset patch
# User wenzelm
# Date 1308262239 -7200
# Node ID c69e9fbb81a85357147ea78dd644d9cde61c911b
# Parent  83be997a11d6604d2739cff33b91a47b62e46cf0
recovered markup for non-alphabetic keywords;

diff -r 83be997a11d6 -r c69e9fbb81a8 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Thu Jun 16 23:35:37 2011 +0200
+++ b/src/Pure/General/symbol.ML	Fri Jun 17 00:10:39 2011 +0200
@@ -134,7 +134,7 @@
 fun malformed_msg s = "Malformed symbolic character: " ^ quote s;
 
 
-(* ascii symbols *)
+(* ASCII symbols *)
 
 fun is_ascii s = is_char s andalso ord s < 128;
 
diff -r 83be997a11d6 -r c69e9fbb81a8 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu Jun 16 23:35:37 2011 +0200
+++ b/src/Pure/General/symbol.scala	Fri Jun 17 00:10:39 2011 +0200
@@ -28,6 +28,19 @@
   }
 
 
+  /* ASCII characters */
+
+  def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
+  def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9'
+  def is_ascii_quasi(c: Char): Boolean = c == '_' || c == '\''
+
+  def is_ascii_letdig(c: Char): Boolean =
+    is_ascii_letter(c) || is_ascii_digit(c) || is_ascii_quasi(c)
+
+  def is_ascii_identifier(s: String): Boolean =
+    s.length > 0 && is_ascii_letter(s(0)) && s.substring(1).forall(is_ascii_letdig)
+
+
   /* Symbol regexps */
 
   private val plain = new Regex("""(?xs)
diff -r 83be997a11d6 -r c69e9fbb81a8 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Thu Jun 16 23:35:37 2011 +0200
+++ b/src/Pure/Isar/token.scala	Fri Jun 17 00:10:39 2011 +0200
@@ -64,6 +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_delimited: Boolean =
     kind == Token.Kind.STRING ||
     kind == Token.Kind.ALT_STRING ||
diff -r 83be997a11d6 -r c69e9fbb81a8 src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Thu Jun 16 23:35:37 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Fri Jun 17 00:10:39 2011 +0200
@@ -215,5 +215,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
     else token_style(token.kind)
 }