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