equal
deleted
inserted
replaced
112 val matcher = |
112 val matcher = |
113 Proof_Document.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start)) |
113 Proof_Document.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start)) |
114 |
114 |
115 while (matcher.find() && invalid_tokens != Nil) { |
115 while (matcher.find() && invalid_tokens != Nil) { |
116 val kind = |
116 val kind = |
117 if (session.keywords.is_command(matcher.group)) |
117 if (session.syntax().is_command(matcher.group)) |
118 Token.Kind.COMMAND_START |
118 Token.Kind.COMMAND_START |
119 else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*") |
119 else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*") |
120 Token.Kind.COMMENT |
120 Token.Kind.COMMENT |
121 else |
121 else |
122 Token.Kind.OTHER |
122 Token.Kind.OTHER |