src/Pure/Tools/bibtex.scala
changeset 58609 d0cb70d66bc1
parent 58596 877c5ecee253
child 59319 677615cba30d
equal deleted inserted replaced
58605:9d5013661ac6 58609:d0cb70d66bc1
   213 
   213 
   214 
   214 
   215     /* ignored text */
   215     /* ignored text */
   216 
   216 
   217     private val ignored: Parser[Chunk] =
   217     private val ignored: Parser[Chunk] =
   218       rep1("""(?mi)([^@]+|@[ \t]*comment)""".r) ^^ {
   218       rep1("""(?i)([^@]+|@[ \t]*comment)""".r) ^^ {
   219         case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) }
   219         case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) }
   220 
   220 
   221     private def ignored_line: Parser[(Chunk, Line_Context)] =
   221     private def ignored_line: Parser[(Chunk, Line_Context)] =
   222       ignored ^^ { case a => (a, Ignored) }
   222       ignored ^^ { case a => (a, Ignored) }
   223 
   223 
   265     private def delimited: Parser[Token] =
   265     private def delimited: Parser[Token] =
   266       delimited_depth(Closed) ^?
   266       delimited_depth(Closed) ^?
   267         { case (s, delim) if delim == Closed => Token(Token.Kind.STRING, s) }
   267         { case (s, delim) if delim == Closed => Token(Token.Kind.STRING, s) }
   268 
   268 
   269     private def recover_delimited: Parser[Token] =
   269     private def recover_delimited: Parser[Token] =
   270       """(?m)["{][^@]*""".r ^^ token(Token.Kind.ERROR)
   270       """["{][^@]*""".r ^^ token(Token.Kind.ERROR)
   271 
   271 
   272     def delimited_line(ctxt: Item): Parser[(Chunk, Line_Context)] =
   272     def delimited_line(ctxt: Item): Parser[(Chunk, Line_Context)] =
   273       delimited_depth(ctxt.delim) ^^ { case (s, delim1) =>
   273       delimited_depth(ctxt.delim) ^^ { case (s, delim1) =>
   274         (Chunk(ctxt.kind, List(Token(Token.Kind.STRING, s))), ctxt.copy(delim = delim1)) } |
   274         (Chunk(ctxt.kind, List(Token(Token.Kind.STRING, s))), ctxt.copy(delim = delim1)) } |
   275       recover_delimited ^^ { case a => (Chunk(ctxt.kind, List(a)), Ignored) }
   275       recover_delimited ^^ { case a => (Chunk(ctxt.kind, List(a)), Ignored) }
   336         { case (kind, a) ~ ((end, b)) ~ c =>
   336         { case (kind, a) ~ ((end, b)) ~ c =>
   337             opt(item_name(kind)) ~ rep(body) ~ opt(end ^^ keyword) ^^ {
   337             opt(item_name(kind)) ~ rep(body) ~ opt(end ^^ keyword) ^^ {
   338               case d ~ e ~ f => Chunk(kind, a ::: List(b) ::: c ::: d.toList ::: e ::: f.toList) } }
   338               case d ~ e ~ f => Chunk(kind, a ::: List(b) ::: c ::: d.toList ::: e ::: f.toList) } }
   339 
   339 
   340     private val recover_item: Parser[Chunk] =
   340     private val recover_item: Parser[Chunk] =
   341       at ~ "(?m)[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) }
   341       at ~ "[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) }
   342 
   342 
   343 
   343 
   344     /* chunks */
   344     /* chunks */
   345 
   345 
   346     val chunk: Parser[Chunk] = ignored | (item | recover_item)
   346     val chunk: Parser[Chunk] = ignored | (item | recover_item)