1.1 --- a/src/Pure/General/symbol.ML	Thu Jun 16 23:35:37 2011 +0200
     1.2 +++ b/src/Pure/General/symbol.ML	Fri Jun 17 00:10:39 2011 +0200
     1.3 @@ -134,7 +134,7 @@
     1.4  fun malformed_msg s = "Malformed symbolic character: " ^ quote s;
     1.5  
     1.6  
     1.7 -(* ascii symbols *)
     1.8 +(* ASCII symbols *)
     1.9  
    1.10  fun is_ascii s = is_char s andalso ord s < 128;
    1.11  

     2.1 --- a/src/Pure/General/symbol.scala	Thu Jun 16 23:35:37 2011 +0200
     2.2 +++ b/src/Pure/General/symbol.scala	Fri Jun 17 00:10:39 2011 +0200
     2.3 @@ -28,6 +28,19 @@
     2.4    }
     2.5  
     2.6  
     2.7 +  /* ASCII characters */
     2.8 +
     2.9 +  def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
    2.10 +  def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9'
    2.11 +  def is_ascii_quasi(c: Char): Boolean = c == '_' || c == '\''
    2.12 +
    2.13 +  def is_ascii_letdig(c: Char): Boolean =
    2.14 +    is_ascii_letter(c) || is_ascii_digit(c) || is_ascii_quasi(c)
    2.15 +
    2.16 +  def is_ascii_identifier(s: String): Boolean =
    2.17 +    s.length > 0 && is_ascii_letter(s(0)) && s.substring(1).forall(is_ascii_letdig)
    2.18 +
    2.19 +
    2.20    /* Symbol regexps */
    2.21  
    2.22    private val plain = new Regex("""(?xs)

     3.1 --- a/src/Pure/Isar/token.scala	Thu Jun 16 23:35:37 2011 +0200
     3.2 +++ b/src/Pure/Isar/token.scala	Fri Jun 17 00:10:39 2011 +0200
     3.3 @@ -64,6 +64,7 @@
     3.4  sealed case class Token(val kind: Token.Kind.Value, val source: String)
     3.5  {
     3.6    def is_command: Boolean = kind == Token.Kind.COMMAND
     3.7 +  def is_keyword: Boolean = kind == Token.Kind.KEYWORD
     3.8    def is_delimited: Boolean =
     3.9      kind == Token.Kind.STRING ||
    3.10      kind == Token.Kind.ALT_STRING ||

     4.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Thu Jun 16 23:35:37 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Fri Jun 17 00:10:39 2011 +0200
     4.3 @@ -215,5 +215,7 @@
     4.4    def token_markup(syntax: Outer_Syntax, token: Token): Byte =
     4.5      if (token.is_command)
     4.6        command_style(syntax.keyword_kind(token.content).getOrElse(""))
     4.7 +    else if (token.is_keyword && !Symbol.is_ascii_identifier(token.content))
     4.8 +      JEditToken.OPERATOR
     4.9      else token_style(token.kind)
    4.10  }