--- a/src/Pure/Tools/bibtex.scala Sat Oct 04 15:11:29 2014 +0200
+++ b/src/Pure/Tools/bibtex.scala Sat Oct 04 15:34:25 2014 +0200
@@ -125,6 +125,7 @@
val KEYWORD = Value("keyword")
val NAT = Value("natural number")
val STRING = Value("string")
+ val NAME = Value("name")
val IDENT = Value("identifier")
val IGNORED = Value("ignored")
val ERROR = Value("bad input")
@@ -137,6 +138,9 @@
kind == Token.Kind.COMMAND ||
kind == Token.Kind.ENTRY ||
kind == Token.Kind.IDENT
+ 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
}
@@ -162,7 +166,7 @@
def name: String =
content match {
- case Some(Token(Token.Kind.IDENT, a) :: _) => a
+ case Some(tok :: _) if tok.is_name => tok.source
case _ => ""
}
@@ -289,17 +293,21 @@
Token(kind, a)
}
- private val item_start: Parser[(String, List[Token])] =
+ private val item_start =
at ~ rep(strict_space) ~ item_kind ~ rep(strict_space) ^^
{ case a ~ b ~ c ~ d => (c.source, List(a) ::: b ::: List(c) ::: d) }
+ private val item_name =
+ rep(strict_space) ~ identifier ^^
+ { case a ~ b => a ::: List(Token(Token.Kind.NAME, b)) }
+
private val item_body =
delimited | (recover_delimited | other_token)
private val item: Parser[Chunk] =
- (item_start ~ left_brace ~ rep(item_body) ~ opt(right_brace) |
- item_start ~ left_paren ~ rep(item_body) ~ opt(right_paren)) ^^
- { case (kind, a) ~ b ~ c ~ d => Chunk(kind, a ::: List(b) ::: c ::: d.toList) }
+ (item_start ~ left_brace ~ item_name ~ rep(item_body) ~ opt(right_brace) |
+ item_start ~ left_paren ~ item_name ~ rep(item_body) ~ opt(right_paren)) ^^
+ { case (kind, a) ~ b ~ c ~ d ~ e => Chunk(kind, a ::: List(b) ::: c ::: d ::: e.toList) }
private val recover_item: Parser[Chunk] =
at ~ "(?m)[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) }
@@ -314,10 +322,11 @@
ctxt match {
case Ignored_Context =>
ignored ^^ { case a => (a, ctxt) } |
- item_start ~ (left_brace | left_paren) ^^
- { case (kind, a) ~ b =>
+ item_start ~ (left_brace | left_paren) ~ opt(item_name) ^^
+ { case (kind, a) ~ b ~ c =>
val right = if (b.source == "{") "}" else ")"
- (Chunk(kind, a ::: List(b)), Item_Context(kind, Closed, right)) } |
+ val chunk = Chunk(kind, a ::: List(b) ::: (c getOrElse Nil))
+ (chunk, Item_Context(kind, Closed, right)) } |
recover_item ^^ { case a => (a, Ignored_Context) }
case Item_Context(kind, delim, right) =>
if (delim.depth > 0)
--- a/src/Tools/jEdit/src/bibtex_token_markup.scala Sat Oct 04 15:11:29 2014 +0200
+++ b/src/Tools/jEdit/src/bibtex_token_markup.scala Sat Oct 04 15:34:25 2014 +0200
@@ -25,6 +25,7 @@
case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR
case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2
case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1
+ case Bibtex.Token.Kind.NAME => JEditToken.LABEL
case Bibtex.Token.Kind.IDENT =>
if (Bibtex.is_month(token.source)) JEditToken.LITERAL3
else