# HG changeset patch # User wenzelm # Date 1412598098 -7200 # Node ID 3c1a8c1c6b3b05846827b1cdcde9d72bded129ae # Parent 472b9fbcc7f06c4cd412e2098d1bdc25e377e020 more accurate item name, depending on kind; tuned; diff -r 472b9fbcc7f0 -r 3c1a8c1c6b3b src/Pure/Tools/bibtex.scala --- a/src/Pure/Tools/bibtex.scala Mon Oct 06 11:44:16 2014 +0200 +++ b/src/Pure/Tools/bibtex.scala Mon Oct 06 14:21:38 2014 +0200 @@ -189,8 +189,8 @@ case object Ignored extends Line_Context case object At extends Line_Context case class Item_Start(kind: String) extends Line_Context - case class Item_Open(kind: String, right: String) extends Line_Context - case class Item(kind: String, right: String, delim: Delimited) extends Line_Context + case class Item_Open(kind: String, end: String) extends Line_Context + case class Item(kind: String, end: String, delim: Delimited) extends Line_Context case class Delimited(quoted: Boolean, depth: Int) val Closed = Delimited(false, 0) @@ -278,13 +278,11 @@ /* other tokens */ private val at = "@" ^^ keyword - private val left_brace = "{" ^^ keyword - private val right_brace = "}" ^^ keyword - private val left_paren = "(" ^^ keyword - private val right_paren = ")" ^^ keyword private val nat = "[0-9]+".r ^^ token(Token.Kind.NAT) + private val name = """[\x21-\x7f&&[^"#%'(),={}]]+""".r ^^ token(Token.Kind.NAME) + private val identifier = """[\x21-\x7f&&[^"#%'(),={}0-9]][\x21-\x7f&&[^"#%'(),={}]]*""".r @@ -293,6 +291,20 @@ val other_token = "[=#,]".r ^^ keyword | (nat | (ident | space)) + /* body */ + + private val body = + delimited | (recover_delimited | other_token) + + private def body_line(ctxt: Item) = + if (ctxt.delim.depth > 0) + delimited_line(ctxt) + else + delimited_line(ctxt) | + other_token ^^ { case a => (Chunk(ctxt.kind, List(a)), ctxt) } | + ctxt.end ^^ { case a => (Chunk(ctxt.kind, List(keyword(a))), Ignored) } + + /* items: command or entry */ private val item_kind = @@ -304,34 +316,32 @@ Token(kind, a) } + private val item_begin = + "{" ^^ { case a => ("}", keyword(a)) } | + "(" ^^ { case a => (")", keyword(a)) } + + private def item_name(kind: String) = + kind.toLowerCase match { + case "preamble" => failure("") + case "string" => identifier ^^ token(Token.Kind.NAME) + case _ => name + } + private val item_start = at ~ spaces ~ item_kind ~ spaces ^^ { case a ~ b ~ c ~ d => (c.source, List(a) ::: b ::: List(c) ::: d) } - private val item_name = identifier ^^ token(Token.Kind.NAME) - - private val item_body = - delimited | (recover_delimited | other_token) - private val item: Parser[Chunk] = - (item_start ~ left_brace ~ spaces ~ item_name ~ rep(item_body) ~ opt(right_brace) | - item_start ~ left_paren ~ spaces ~ item_name ~ rep(item_body) ~ opt(right_paren)) ^^ - { case (kind, a) ~ b ~ c ~ d ~ e ~ f => - Chunk(kind, a ::: List(b) ::: c ::: List(d) ::: e ::: f.toList) } - - - /* chunks */ + (item_start ~ item_begin ~ spaces) into + { case (kind, a) ~ ((end, b)) ~ c => + opt(item_name(kind)) ~ rep(body) ~ opt(end ^^ keyword) ^^ { + case d ~ e ~ f => Chunk(kind, a ::: List(b) ::: c ::: d.toList ::: e ::: f.toList) } } private val recover_item: Parser[Chunk] = at ~ "(?m)[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) } - private def item_body_line(ctxt: Item) = - if (ctxt.delim.depth > 0) - delimited_line(ctxt) - else - delimited_line(ctxt) | - other_token ^^ { case a => (Chunk(ctxt.kind, List(a)), ctxt) } | - ctxt.right ^^ { case a => (Chunk(ctxt.kind, List(keyword(a))), Ignored) } + + /* chunks */ val chunk: Parser[Chunk] = ignored | (item | recover_item) @@ -350,18 +360,17 @@ case Item_Start(kind) => space ^^ { case a => (Chunk(kind, List(a)), ctxt) } | - left_brace ^^ { case a => (Chunk(kind, List(a)), Item_Open(kind, "}")) } | - left_paren ^^ { case a => (Chunk(kind, List(a)), Item_Open(kind, ")")) } | + item_begin ^^ { case (end, a) => (Chunk(kind, List(a)), Item_Open(kind, end)) } | ignored_line - case Item_Open(kind, right) => + case Item_Open(kind, end) => space ^^ { case a => (Chunk(kind, List(a)), ctxt) } | - item_name ^^ { case a => (Chunk(kind, List(a)), Item(kind, right, Closed)) } | - item_body_line(Item(kind, right, Closed)) | + item_name(kind) ^^ { case a => (Chunk(kind, List(a)), Item(kind, end, Closed)) } | + body_line(Item(kind, end, Closed)) | ignored_line case item_ctxt: Item => - item_body_line(item_ctxt) | + body_line(item_ctxt) | ignored_line case _ => failure("")