--- a/src/Pure/Tools/bibtex.scala Mon Oct 06 21:21:46 2014 +0200
+++ b/src/Pure/Tools/bibtex.scala Tue Oct 07 11:44:25 2014 +0200
@@ -215,7 +215,7 @@
/* ignored text */
private val ignored: Parser[Chunk] =
- rep1("""(?mi)([^@]+|@[ \t]*comment)""".r) ^^ {
+ rep1("""(?i)([^@]+|@[ \t]*comment)""".r) ^^ {
case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) }
private def ignored_line: Parser[(Chunk, Line_Context)] =
@@ -267,7 +267,7 @@
{ case (s, delim) if delim == Closed => Token(Token.Kind.STRING, s) }
private def recover_delimited: Parser[Token] =
- """(?m)["{][^@]*""".r ^^ token(Token.Kind.ERROR)
+ """["{][^@]*""".r ^^ token(Token.Kind.ERROR)
def delimited_line(ctxt: Item): Parser[(Chunk, Line_Context)] =
delimited_depth(ctxt.delim) ^^ { case (s, delim1) =>
@@ -338,7 +338,7 @@
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))) }
+ at ~ "[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) }
/* chunks */