# HG changeset patch
# User wenzelm
# Date 1412438730 -7200
# Node ID 4815429974fe3ffffcbbbfff6380a8045f997196
# Parent  573ce5ad13bc084b69c7ce89915b767a83ed08e5
more explicit comments;

diff -r 573ce5ad13bc -r 4815429974fe src/Pure/Tools/bibtex.scala
--- a/src/Pure/Tools/bibtex.scala	Sat Oct 04 17:57:03 2014 +0200
+++ b/src/Pure/Tools/bibtex.scala	Sat Oct 04 18:05:30 2014 +0200
@@ -127,7 +127,8 @@
       val STRING = Value("string")
       val NAME = Value("name")
       val IDENT = Value("identifier")
-      val IGNORED = Value("ignored")
+      val SPACE = Value("white space")
+      val COMMENT = Value("ignored text")
       val ERROR = Value("bad input")
     }
   }
@@ -141,8 +142,11 @@
     def is_name: Boolean =
       kind == Token.Kind.NAME ||
       kind == Token.Kind.IDENT
-    def is_ignored: Boolean = kind == Token.Kind.IGNORED
-    def is_malformed: Boolean = kind == Token.Kind.ERROR
+    def is_ignored: Boolean =
+      kind == Token.Kind.SPACE ||
+      kind == Token.Kind.COMMENT
+    def is_malformed: Boolean = kind ==
+      Token.Kind.ERROR
   }
 
   case class Chunk(kind: String, tokens: List[Token])
@@ -202,15 +206,15 @@
 
     override val whiteSpace = "".r
 
-    private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.IGNORED)
-    private val strict_space = """[ \t]+""".r ^^ token(Token.Kind.IGNORED)
+    private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.SPACE)
+    private val strict_space = """[ \t]+""".r ^^ token(Token.Kind.SPACE)
 
 
-    /* ignored material */
+    /* ignored text */
 
     private val ignored: Parser[Chunk] =
       rep1("""(?mi)([^@]+|@[ \t]*comment)""".r) ^^ {
-        case ss => Chunk("", List(Token(Token.Kind.IGNORED, ss.mkString))) }
+        case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) }
 
 
     /* delimited string: outermost "..." or {...} and body with balanced {...} */
diff -r 573ce5ad13bc -r 4815429974fe src/Tools/jEdit/src/bibtex_token_markup.scala
--- a/src/Tools/jEdit/src/bibtex_token_markup.scala	Sat Oct 04 17:57:03 2014 +0200
+++ b/src/Tools/jEdit/src/bibtex_token_markup.scala	Sat Oct 04 18:05:30 2014 +0200
@@ -34,7 +34,8 @@
             case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4
             case _ => JEditToken.DIGIT
           }
-      case Bibtex.Token.Kind.IGNORED => JEditToken.NULL
+      case Bibtex.Token.Kind.SPACE => JEditToken.NULL
+      case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1
       case Bibtex.Token.Kind.ERROR => JEditToken.INVALID
     }