src/Pure/Tools/bibtex.scala
author wenzelm
Mon Dec 22 16:44:24 2014 +0100 (2014-12-22 ago)
changeset 59175 bf465f335e85
parent 58609 d0cb70d66bc1
child 59319 677615cba30d
permissions -rw-r--r--
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm@58523
     1
/*  Title:      Pure/Tools/bibtex.scala
wenzelm@58523
     2
    Author:     Makarius
wenzelm@58523
     3
wenzelm@58544
     4
BibTeX support.
wenzelm@58523
     5
*/
wenzelm@58523
     6
wenzelm@58523
     7
package isabelle
wenzelm@58523
     8
wenzelm@58523
     9
wenzelm@58528
    10
import scala.collection.mutable
wenzelm@58523
    11
import scala.util.parsing.input.{Reader, CharSequenceReader}
wenzelm@58523
    12
import scala.util.parsing.combinator.RegexParsers
wenzelm@58523
    13
wenzelm@58523
    14
wenzelm@58523
    15
object Bibtex
wenzelm@58523
    16
{
wenzelm@58523
    17
  /** content **/
wenzelm@58523
    18
wenzelm@58529
    19
  private val months = List(
wenzelm@58523
    20
    "jan",
wenzelm@58523
    21
    "feb",
wenzelm@58523
    22
    "mar",
wenzelm@58523
    23
    "apr",
wenzelm@58523
    24
    "may",
wenzelm@58523
    25
    "jun",
wenzelm@58523
    26
    "jul",
wenzelm@58523
    27
    "aug",
wenzelm@58523
    28
    "sep",
wenzelm@58523
    29
    "oct",
wenzelm@58523
    30
    "nov",
wenzelm@58523
    31
    "dec")
wenzelm@58529
    32
  def is_month(s: String): Boolean = months.contains(s.toLowerCase)
wenzelm@58523
    33
wenzelm@58529
    34
  private val commands = List("preamble", "string")
wenzelm@58529
    35
  def is_command(s: String): Boolean = commands.contains(s.toLowerCase)
wenzelm@58523
    36
wenzelm@58524
    37
  sealed case class Entry(
wenzelm@58526
    38
    kind: String,
wenzelm@58523
    39
    required: List[String],
wenzelm@58523
    40
    optional_crossref: List[String],
wenzelm@58529
    41
    optional_other: List[String])
wenzelm@58524
    42
  {
wenzelm@58533
    43
    def is_required(s: String): Boolean = required.contains(s.toLowerCase)
wenzelm@58529
    44
    def is_optional(s: String): Boolean =
wenzelm@58533
    45
      optional_crossref.contains(s.toLowerCase) || optional_other.contains(s.toLowerCase)
wenzelm@58529
    46
wenzelm@58529
    47
    def fields: List[String] = required ::: optional_crossref ::: optional_other
wenzelm@58524
    48
    def template: String =
wenzelm@58526
    49
      "@" + kind + "{,\n" + fields.map(x => "  " + x + " = {},\n").mkString + "}\n"
wenzelm@58524
    50
  }
wenzelm@58523
    51
wenzelm@58524
    52
  val entries: List[Entry] =
wenzelm@58524
    53
    List(
wenzelm@58524
    54
      Entry("Article",
wenzelm@58524
    55
        List("author", "title"),
wenzelm@58524
    56
        List("journal", "year"),
wenzelm@58524
    57
        List("volume", "number", "pages", "month", "note")),
wenzelm@58524
    58
      Entry("InProceedings",
wenzelm@58524
    59
        List("author", "title"),
wenzelm@58524
    60
        List("booktitle", "year"),
wenzelm@58524
    61
        List("editor", "volume", "number", "series", "pages", "month", "address",
wenzelm@58524
    62
          "organization", "publisher", "note")),
wenzelm@58524
    63
      Entry("InCollection",
wenzelm@58524
    64
        List("author", "title", "booktitle"),
wenzelm@58524
    65
        List("publisher", "year"),
wenzelm@58524
    66
        List("editor", "volume", "number", "series", "type", "chapter", "pages",
wenzelm@58524
    67
          "edition", "month", "address", "note")),
wenzelm@58524
    68
      Entry("InBook",
wenzelm@58524
    69
        List("author", "editor", "title", "chapter"),
wenzelm@58524
    70
        List("publisher", "year"),
wenzelm@58524
    71
        List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")),
wenzelm@58524
    72
      Entry("Proceedings",
wenzelm@58524
    73
        List("title", "year"),
wenzelm@58524
    74
        List(),
wenzelm@58524
    75
        List("booktitle", "editor", "volume", "number", "series", "address", "month",
wenzelm@58524
    76
          "organization", "publisher", "note")),
wenzelm@58524
    77
      Entry("Book",
wenzelm@58524
    78
        List("author", "editor", "title"),
wenzelm@58524
    79
        List("publisher", "year"),
wenzelm@58524
    80
        List("volume", "number", "series", "address", "edition", "month", "note")),
wenzelm@58524
    81
      Entry("Booklet",
wenzelm@58524
    82
        List("title"),
wenzelm@58524
    83
        List(),
wenzelm@58524
    84
        List("author", "howpublished", "address", "month", "year", "note")),
wenzelm@58524
    85
      Entry("PhdThesis",
wenzelm@58524
    86
        List("author", "title", "school", "year"),
wenzelm@58524
    87
        List(),
wenzelm@58524
    88
        List("type", "address", "month", "note")),
wenzelm@58524
    89
      Entry("MastersThesis",
wenzelm@58524
    90
        List("author", "title", "school", "year"),
wenzelm@58524
    91
        List(),
wenzelm@58524
    92
        List("type", "address", "month", "note")),
wenzelm@58524
    93
      Entry("TechReport",
wenzelm@58524
    94
        List("author", "title", "institution", "year"),
wenzelm@58524
    95
        List(),
wenzelm@58524
    96
        List("type", "number", "address", "month", "note")),
wenzelm@58524
    97
      Entry("Manual",
wenzelm@58524
    98
        List("title"),
wenzelm@58524
    99
        List(),
wenzelm@58524
   100
        List("author", "organization", "address", "edition", "month", "year", "note")),
wenzelm@58524
   101
      Entry("Unpublished",
wenzelm@58524
   102
        List("author", "title", "note"),
wenzelm@58524
   103
        List(),
wenzelm@58524
   104
        List("month", "year")),
wenzelm@58524
   105
      Entry("Misc",
wenzelm@58524
   106
        List(),
wenzelm@58524
   107
        List(),
wenzelm@58524
   108
        List("author", "title", "howpublished", "month", "year", "note")))
wenzelm@58523
   109
wenzelm@58529
   110
  def get_entry(kind: String): Option[Entry] =
wenzelm@58529
   111
    entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase)
wenzelm@58529
   112
wenzelm@58530
   113
  def is_entry(kind: String): Boolean = get_entry(kind).isDefined
wenzelm@58530
   114
wenzelm@58523
   115
wenzelm@58523
   116
wenzelm@58523
   117
  /** tokens and chunks **/
wenzelm@58523
   118
wenzelm@58523
   119
  object Token
wenzelm@58523
   120
  {
wenzelm@58523
   121
    object Kind extends Enumeration
wenzelm@58523
   122
    {
wenzelm@58529
   123
      val COMMAND = Value("command")
wenzelm@58529
   124
      val ENTRY = Value("entry")
wenzelm@58523
   125
      val KEYWORD = Value("keyword")
wenzelm@58523
   126
      val NAT = Value("natural number")
wenzelm@58529
   127
      val STRING = Value("string")
wenzelm@58531
   128
      val NAME = Value("name")
wenzelm@58523
   129
      val IDENT = Value("identifier")
wenzelm@58535
   130
      val SPACE = Value("white space")
wenzelm@58535
   131
      val COMMENT = Value("ignored text")
wenzelm@58523
   132
      val ERROR = Value("bad input")
wenzelm@58523
   133
    }
wenzelm@58523
   134
  }
wenzelm@58523
   135
wenzelm@58523
   136
  sealed case class Token(kind: Token.Kind.Value, val source: String)
wenzelm@58523
   137
  {
wenzelm@58530
   138
    def is_kind: Boolean =
wenzelm@58530
   139
      kind == Token.Kind.COMMAND ||
wenzelm@58530
   140
      kind == Token.Kind.ENTRY ||
wenzelm@58530
   141
      kind == Token.Kind.IDENT
wenzelm@58531
   142
    def is_name: Boolean =
wenzelm@58531
   143
      kind == Token.Kind.NAME ||
wenzelm@58531
   144
      kind == Token.Kind.IDENT
wenzelm@58535
   145
    def is_ignored: Boolean =
wenzelm@58535
   146
      kind == Token.Kind.SPACE ||
wenzelm@58535
   147
      kind == Token.Kind.COMMENT
wenzelm@58535
   148
    def is_malformed: Boolean = kind ==
wenzelm@58535
   149
      Token.Kind.ERROR
wenzelm@58523
   150
  }
wenzelm@58523
   151
wenzelm@58530
   152
  case class Chunk(kind: String, tokens: List[Token])
wenzelm@58523
   153
  {
wenzelm@58529
   154
    val source = tokens.map(_.source).mkString
wenzelm@58526
   155
wenzelm@58530
   156
    private val content: Option[List[Token]] =
wenzelm@58523
   157
      tokens match {
wenzelm@58530
   158
        case Token(Token.Kind.KEYWORD, "@") :: body if !body.isEmpty =>
wenzelm@58529
   159
          (body.init.filterNot(_.is_ignored), body.last) match {
wenzelm@58530
   160
            case (tok :: Token(Token.Kind.KEYWORD, "{") :: toks, Token(Token.Kind.KEYWORD, "}"))
wenzelm@58530
   161
            if tok.is_kind => Some(toks)
wenzelm@58530
   162
wenzelm@58530
   163
            case (tok :: Token(Token.Kind.KEYWORD, "(") :: toks, Token(Token.Kind.KEYWORD, ")"))
wenzelm@58530
   164
            if tok.is_kind => Some(toks)
wenzelm@58530
   165
wenzelm@58528
   166
            case _ => None
wenzelm@58523
   167
          }
wenzelm@58528
   168
        case _ => None
wenzelm@58526
   169
      }
wenzelm@58526
   170
wenzelm@58526
   171
    def name: String =
wenzelm@58530
   172
      content match {
wenzelm@58531
   173
        case Some(tok :: _) if tok.is_name => tok.source
wenzelm@58523
   174
        case _ => ""
wenzelm@58523
   175
      }
wenzelm@58530
   176
wenzelm@58530
   177
    def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
wenzelm@58530
   178
    def is_malformed: Boolean = kind == "" || tokens.exists(_.is_malformed)
wenzelm@58543
   179
    def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined
wenzelm@58543
   180
    def is_entry: Boolean = Bibtex.is_entry(kind) && name != "" && content.isDefined
wenzelm@58523
   181
  }
wenzelm@58523
   182
wenzelm@58523
   183
wenzelm@58523
   184
wenzelm@58523
   185
  /** parsing **/
wenzelm@58523
   186
wenzelm@58523
   187
  // context of partial line-oriented scans
wenzelm@58523
   188
  abstract class Line_Context
wenzelm@58589
   189
  case object Ignored extends Line_Context
wenzelm@58590
   190
  case object At extends Line_Context
wenzelm@58590
   191
  case class Item_Start(kind: String) extends Line_Context
wenzelm@58591
   192
  case class Item_Open(kind: String, end: String) extends Line_Context
wenzelm@58591
   193
  case class Item(kind: String, end: String, delim: Delimited) extends Line_Context
wenzelm@58590
   194
wenzelm@58528
   195
  case class Delimited(quoted: Boolean, depth: Int)
wenzelm@58528
   196
  val Closed = Delimited(false, 0)
wenzelm@58523
   197
wenzelm@58523
   198
  private def token(kind: Token.Kind.Value)(source: String): Token = Token(kind, source)
wenzelm@58523
   199
  private def keyword(source: String): Token = Token(Token.Kind.KEYWORD, source)
wenzelm@58523
   200
wenzelm@58523
   201
wenzelm@58523
   202
  // See also http://ctan.org/tex-archive/biblio/bibtex/base/bibtex.web
wenzelm@58523
   203
  // module @<Scan for and process a \.{.bib} command or database entry@>.
wenzelm@58523
   204
wenzelm@58523
   205
  object Parsers extends RegexParsers
wenzelm@58523
   206
  {
wenzelm@58523
   207
    /* white space and comments */
wenzelm@58523
   208
wenzelm@58523
   209
    override val whiteSpace = "".r
wenzelm@58523
   210
wenzelm@58535
   211
    private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.SPACE)
wenzelm@58590
   212
    private val spaces = rep(space)
wenzelm@58523
   213
wenzelm@58528
   214
wenzelm@58535
   215
    /* ignored text */
wenzelm@58528
   216
wenzelm@58528
   217
    private val ignored: Parser[Chunk] =
wenzelm@58609
   218
      rep1("""(?i)([^@]+|@[ \t]*comment)""".r) ^^ {
wenzelm@58535
   219
        case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) }
wenzelm@58523
   220
wenzelm@58536
   221
    private def ignored_line: Parser[(Chunk, Line_Context)] =
wenzelm@58589
   222
      ignored ^^ { case a => (a, Ignored) }
wenzelm@58536
   223
wenzelm@58523
   224
wenzelm@58523
   225
    /* delimited string: outermost "..." or {...} and body with balanced {...} */
wenzelm@58523
   226
wenzelm@58534
   227
    // see also bibtex.web: scan_a_field_token_and_eat_white, scan_balanced_braces
wenzelm@58523
   228
    private def delimited_depth(delim: Delimited): Parser[(String, Delimited)] =
wenzelm@58523
   229
      new Parser[(String, Delimited)]
wenzelm@58523
   230
      {
wenzelm@58523
   231
        require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0)
wenzelm@58523
   232
wenzelm@58523
   233
        def apply(in: Input) =
wenzelm@58523
   234
        {
wenzelm@58523
   235
          val start = in.offset
wenzelm@58523
   236
          val end = in.source.length
wenzelm@58523
   237
wenzelm@58523
   238
          var i = start
wenzelm@58523
   239
          var q = delim.quoted
wenzelm@58523
   240
          var d = delim.depth
wenzelm@58523
   241
          var finished = false
wenzelm@58523
   242
          while (!finished && i < end) {
wenzelm@58523
   243
            val c = in.source.charAt(i)
wenzelm@58534
   244
wenzelm@58523
   245
            if (c == '"' && d == 0) { i += 1; d = 1; q = true }
wenzelm@58532
   246
            else if (c == '"' && d == 1 && q) {
wenzelm@58532
   247
              i += 1; d = 0; q = false; finished = true
wenzelm@58532
   248
            }
wenzelm@58523
   249
            else if (c == '{') { i += 1; d += 1 }
wenzelm@58534
   250
            else if (c == '}') {
wenzelm@58534
   251
              if (d == 1 && !q || d > 1) { i += 1; d -= 1; if (d == 0) finished = true }
wenzelm@58534
   252
              else {i = start; finished = true }
wenzelm@58532
   253
            }
wenzelm@58523
   254
            else if (d > 0) i += 1
wenzelm@58523
   255
            else finished = true
wenzelm@58523
   256
          }
wenzelm@58523
   257
          if (i == start) Failure("bad input", in)
wenzelm@58528
   258
          else {
wenzelm@58528
   259
            val s = in.source.subSequence(start, i).toString
wenzelm@58528
   260
            Success((s, Delimited(q, d)), in.drop(i - start))
wenzelm@58528
   261
          }
wenzelm@58523
   262
        }
wenzelm@58523
   263
      }.named("delimited_depth")
wenzelm@58523
   264
wenzelm@58528
   265
    private def delimited: Parser[Token] =
wenzelm@58528
   266
      delimited_depth(Closed) ^?
wenzelm@58528
   267
        { case (s, delim) if delim == Closed => Token(Token.Kind.STRING, s) }
wenzelm@58523
   268
wenzelm@58534
   269
    private def recover_delimited: Parser[Token] =
wenzelm@58609
   270
      """["{][^@]*""".r ^^ token(Token.Kind.ERROR)
wenzelm@58534
   271
wenzelm@58590
   272
    def delimited_line(ctxt: Item): Parser[(Chunk, Line_Context)] =
wenzelm@58590
   273
      delimited_depth(ctxt.delim) ^^ { case (s, delim1) =>
wenzelm@58590
   274
        (Chunk(ctxt.kind, List(Token(Token.Kind.STRING, s))), ctxt.copy(delim = delim1)) } |
wenzelm@58590
   275
      recover_delimited ^^ { case a => (Chunk(ctxt.kind, List(a)), Ignored) }
wenzelm@58523
   276
wenzelm@58523
   277
wenzelm@58523
   278
    /* other tokens */
wenzelm@58523
   279
wenzelm@58523
   280
    private val at = "@" ^^ keyword
wenzelm@58523
   281
wenzelm@58523
   282
    private val nat = "[0-9]+".r ^^ token(Token.Kind.NAT)
wenzelm@58523
   283
wenzelm@58591
   284
    private val name = """[\x21-\x7f&&[^"#%'(),={}]]+""".r ^^ token(Token.Kind.NAME)
wenzelm@58591
   285
wenzelm@58529
   286
    private val identifier =
wenzelm@58529
   287
      """[\x21-\x7f&&[^"#%'(),={}0-9]][\x21-\x7f&&[^"#%'(),={}]]*""".r
wenzelm@58529
   288
wenzelm@58529
   289
    private val ident = identifier ^^ token(Token.Kind.IDENT)
wenzelm@58523
   290
wenzelm@58528
   291
    val other_token = "[=#,]".r ^^ keyword | (nat | (ident | space))
wenzelm@58528
   292
wenzelm@58528
   293
wenzelm@58591
   294
    /* body */
wenzelm@58591
   295
wenzelm@58591
   296
    private val body =
wenzelm@58591
   297
      delimited | (recover_delimited | other_token)
wenzelm@58591
   298
wenzelm@58591
   299
    private def body_line(ctxt: Item) =
wenzelm@58591
   300
      if (ctxt.delim.depth > 0)
wenzelm@58591
   301
        delimited_line(ctxt)
wenzelm@58591
   302
      else
wenzelm@58591
   303
        delimited_line(ctxt) |
wenzelm@58591
   304
        other_token ^^ { case a => (Chunk(ctxt.kind, List(a)), ctxt) } |
wenzelm@58591
   305
        ctxt.end ^^ { case a => (Chunk(ctxt.kind, List(keyword(a))), Ignored) }
wenzelm@58591
   306
wenzelm@58591
   307
wenzelm@58530
   308
    /* items: command or entry */
wenzelm@58528
   309
wenzelm@58530
   310
    private val item_kind =
wenzelm@58529
   311
      identifier ^^ { case a =>
wenzelm@58529
   312
        val kind =
wenzelm@58529
   313
          if (is_command(a)) Token.Kind.COMMAND
wenzelm@58530
   314
          else if (is_entry(a)) Token.Kind.ENTRY
wenzelm@58529
   315
          else Token.Kind.IDENT
wenzelm@58529
   316
        Token(kind, a)
wenzelm@58529
   317
      }
wenzelm@58529
   318
wenzelm@58591
   319
    private val item_begin =
wenzelm@58591
   320
      "{" ^^ { case a => ("}", keyword(a)) } |
wenzelm@58591
   321
      "(" ^^ { case a => (")", keyword(a)) }
wenzelm@58591
   322
wenzelm@58591
   323
    private def item_name(kind: String) =
wenzelm@58591
   324
      kind.toLowerCase match {
wenzelm@58591
   325
        case "preamble" => failure("")
wenzelm@58591
   326
        case "string" => identifier ^^ token(Token.Kind.NAME)
wenzelm@58591
   327
        case _ => name
wenzelm@58591
   328
      }
wenzelm@58591
   329
wenzelm@58531
   330
    private val item_start =
wenzelm@58590
   331
      at ~ spaces ~ item_kind ~ spaces ^^
wenzelm@58528
   332
        { case a ~ b ~ c ~ d => (c.source, List(a) ::: b ::: List(c) ::: d) }
wenzelm@58528
   333
wenzelm@58530
   334
    private val item: Parser[Chunk] =
wenzelm@58591
   335
      (item_start ~ item_begin ~ spaces) into
wenzelm@58591
   336
        { case (kind, a) ~ ((end, b)) ~ c =>
wenzelm@58591
   337
            opt(item_name(kind)) ~ rep(body) ~ opt(end ^^ keyword) ^^ {
wenzelm@58591
   338
              case d ~ e ~ f => Chunk(kind, a ::: List(b) ::: c ::: d.toList ::: e ::: f.toList) } }
wenzelm@58528
   339
wenzelm@58530
   340
    private val recover_item: Parser[Chunk] =
wenzelm@58609
   341
      at ~ "[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) }
wenzelm@58528
   342
wenzelm@58591
   343
wenzelm@58591
   344
    /* chunks */
wenzelm@58523
   345
wenzelm@58528
   346
    val chunk: Parser[Chunk] = ignored | (item | recover_item)
wenzelm@58523
   347
wenzelm@58528
   348
    def chunk_line(ctxt: Line_Context): Parser[(Chunk, Line_Context)] =
wenzelm@58530
   349
    {
wenzelm@58530
   350
      ctxt match {
wenzelm@58589
   351
        case Ignored =>
wenzelm@58538
   352
          ignored_line |
wenzelm@58590
   353
          at ^^ { case a => (Chunk("", List(a)), At) }
wenzelm@58590
   354
wenzelm@58590
   355
        case At =>
wenzelm@58590
   356
          space ^^ { case a => (Chunk("", List(a)), ctxt) } |
wenzelm@58590
   357
          item_kind ^^ { case a => (Chunk(a.source, List(a)), Item_Start(a.source)) } |
wenzelm@58590
   358
          recover_item ^^ { case a => (a, Ignored) } |
wenzelm@58590
   359
          ignored_line
wenzelm@58590
   360
wenzelm@58590
   361
        case Item_Start(kind) =>
wenzelm@58590
   362
          space ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
wenzelm@58591
   363
          item_begin ^^ { case (end, a) => (Chunk(kind, List(a)), Item_Open(kind, end)) } |
wenzelm@58596
   364
          recover_item ^^ { case a => (a, Ignored) } |
wenzelm@58590
   365
          ignored_line
wenzelm@58590
   366
wenzelm@58591
   367
        case Item_Open(kind, end) =>
wenzelm@58590
   368
          space ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
wenzelm@58591
   369
          item_name(kind) ^^ { case a => (Chunk(kind, List(a)), Item(kind, end, Closed)) } |
wenzelm@58591
   370
          body_line(Item(kind, end, Closed)) |
wenzelm@58590
   371
          ignored_line
wenzelm@58590
   372
wenzelm@58590
   373
        case item_ctxt: Item =>
wenzelm@58591
   374
          body_line(item_ctxt) |
wenzelm@58590
   375
          ignored_line
wenzelm@58590
   376
wenzelm@58530
   377
        case _ => failure("")
wenzelm@58530
   378
      }
wenzelm@58530
   379
    }
wenzelm@58528
   380
  }
wenzelm@58523
   381
wenzelm@58523
   382
wenzelm@58528
   383
  /* parse */
wenzelm@58523
   384
wenzelm@58523
   385
  def parse(input: CharSequence): List[Chunk] =
wenzelm@58523
   386
  {
wenzelm@58523
   387
    val in: Reader[Char] = new CharSequenceReader(input)
wenzelm@58528
   388
    Parsers.parseAll(Parsers.rep(Parsers.chunk), in) match {
wenzelm@58523
   389
      case Parsers.Success(result, _) => result
wenzelm@58526
   390
      case _ => error("Unexpected failure to parse input:\n" + input.toString)
wenzelm@58523
   391
    }
wenzelm@58523
   392
  }
wenzelm@58528
   393
wenzelm@58528
   394
  def parse_line(input: CharSequence, context: Line_Context): (List[Chunk], Line_Context) =
wenzelm@58528
   395
  {
wenzelm@58528
   396
    var in: Reader[Char] = new CharSequenceReader(input)
wenzelm@58528
   397
    val chunks = new mutable.ListBuffer[Chunk]
wenzelm@58528
   398
    var ctxt = context
wenzelm@58528
   399
    while (!in.atEnd) {
wenzelm@58528
   400
      Parsers.parse(Parsers.chunk_line(ctxt), in) match {
wenzelm@58528
   401
        case Parsers.Success((x, c), rest) => { chunks += x; ctxt = c; in = rest }
wenzelm@58528
   402
        case Parsers.NoSuccess(_, rest) =>
wenzelm@58528
   403
          error("Unepected failure to parse input:\n" + rest.source.toString)
wenzelm@58528
   404
      }
wenzelm@58528
   405
    }
wenzelm@58528
   406
    (chunks.toList, ctxt)
wenzelm@58528
   407
  }
wenzelm@58523
   408
}
wenzelm@58523
   409