src/Pure/Thy/bibtex.scala
author wenzelm
Sat, 28 Nov 2020 15:17:14 +0100
changeset 72756 72ac27ea12b2
parent 72729 83411077c37b
child 72836 ec61e1767689
permissions -rw-r--r--
more positions;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
67274
4588f714a78a clarified directories;
wenzelm
parents: 67272
diff changeset
     1
/*  Title:      Pure/Thy/bibtex.scala
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
     3
58544
340f130b3d38 bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents: 58543
diff changeset
     4
BibTeX support.
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
     5
*/
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
     6
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
     7
package isabelle
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
     8
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
     9
67290
98b6cd12f963 implicit thy_load context for bibtex files;
wenzelm
parents: 67289
diff changeset
    10
import java.io.{File => JFile}
98b6cd12f963 implicit thy_load context for bibtex files;
wenzelm
parents: 67289
diff changeset
    11
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
    12
import scala.collection.mutable
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
    13
import scala.util.parsing.combinator.RegexParsers
64824
330ec9bc4b75 tuned signature;
wenzelm
parents: 60215
diff changeset
    14
import scala.util.parsing.input.Reader
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
    15
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
    16
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
    17
object Bibtex
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
    18
{
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    19
  /** file format **/
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    20
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    21
  def is_bibtex(name: String): Boolean = name.endsWith(".bib")
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    22
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    23
  class File_Format extends isabelle.File_Format
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    24
  {
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    25
    val format_name: String = "bibtex"
69257
039edba27102 clarified signature;
wenzelm
parents: 69255
diff changeset
    26
    val file_ext: String = "bib"
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    27
69257
039edba27102 clarified signature;
wenzelm
parents: 69255
diff changeset
    28
    override def theory_suffix: String = "bibtex_file"
69259
wenzelm
parents: 69257
diff changeset
    29
    override def theory_content(name: String): String =
wenzelm
parents: 69257
diff changeset
    30
      """theory "bib" imports Pure begin bibtex_file """ + quote(name) + """ end"""
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    31
72652
07edf1952ab1 clarified modules;
wenzelm
parents: 72194
diff changeset
    32
    override def make_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] =
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    33
    {
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    34
      val name = snapshot.node_name
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    35
      if (detect(name.node)) {
69366
b6dacf6eabe3 clarified signature;
wenzelm
parents: 69294
diff changeset
    36
        val title = "Bibliography " + quote(snapshot.node_name.path.file_name)
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    37
        val content =
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    38
          Isabelle_System.with_tmp_file("bib", "bib") { bib =>
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    39
            File.write(bib, snapshot.node.source)
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    40
            Bibtex.html_output(List(bib), style = "unsort", title = title)
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    41
          }
72652
07edf1952ab1 clarified modules;
wenzelm
parents: 72194
diff changeset
    42
        Some(Presentation.Preview(title, content))
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    43
      }
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    44
      else None
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    45
    }
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    46
  }
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    47
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    48
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68224
diff changeset
    49
67203
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    50
  /** bibtex errors **/
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    51
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    52
  def bibtex_errors(dir: Path, root_name: String): List[String] =
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    53
  {
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    54
    val log_path = dir + Path.explode(root_name).ext("blg")
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    55
    if (log_path.is_file) {
67300
0bfbf5b9d6ba more accurate message patterns;
wenzelm
parents: 67293
diff changeset
    56
      val Error1 = """^(I couldn't open database file .+)$""".r
0bfbf5b9d6ba more accurate message patterns;
wenzelm
parents: 67293
diff changeset
    57
      val Error2 = """^(.+)---line (\d+) of file (.+)""".r
67203
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    58
      Line.logical_lines(File.read(log_path)).flatMap(line =>
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    59
        line match {
67300
0bfbf5b9d6ba more accurate message patterns;
wenzelm
parents: 67293
diff changeset
    60
          case Error1(msg) => Some("Bibtex error: " + msg)
0bfbf5b9d6ba more accurate message patterns;
wenzelm
parents: 67293
diff changeset
    61
          case Error2(msg, Value.Int(l), file) =>
67203
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    62
            val path = File.standard_path(file)
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    63
            if (Path.is_wellformed(path)) {
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    64
              val pos = Position.Line_File(l, (dir + Path.explode(path)).canonical.implode)
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    65
              Some("Bibtex error" + Position.here(pos) + ":\n  " + msg)
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    66
            }
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    67
            else None
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    68
          case _ => None
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    69
        })
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    70
    }
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    71
    else Nil
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    72
  }
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    73
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    74
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67014
diff changeset
    75
67272
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    76
  /** check database **/
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    77
67301
e255c76db052 clarified signature;
wenzelm
parents: 67300
diff changeset
    78
  def check_database(database: String): (List[(String, Position.T)], List[(String, Position.T)]) =
67272
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    79
  {
67275
5e427586cb57 check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents: 67274
diff changeset
    80
    val chunks = parse(Line.normalize(database))
5e427586cb57 check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents: 67274
diff changeset
    81
    var chunk_pos = Map.empty[String, Position.T]
67272
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    82
    val tokens = new mutable.ListBuffer[(Token, Position.T)]
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    83
    var line = 1
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    84
    var offset = 1
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    85
67276
abac35ee3565 clarified positions;
wenzelm
parents: 67275
diff changeset
    86
    def make_pos(length: Int): Position.T =
abac35ee3565 clarified positions;
wenzelm
parents: 67275
diff changeset
    87
      Position.Offset(offset) ::: Position.End_Offset(offset + length) ::: Position.Line(line)
67272
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    88
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    89
    def advance_pos(tok: Token)
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    90
    {
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    91
      for (s <- Symbol.iterator(tok.source)) {
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    92
        if (Symbol.is_newline(s)) line += 1
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    93
        offset += 1
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    94
      }
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    95
    }
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    96
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    97
    def get_line_pos(l: Int): Position.T =
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    98
      if (0 < l && l <= tokens.length) tokens(l - 1)._2 else Position.none
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
    99
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   100
    for (chunk <- chunks) {
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   101
      val name = chunk.name
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   102
      if (name != "" && !chunk_pos.isDefinedAt(name)) {
67276
abac35ee3565 clarified positions;
wenzelm
parents: 67275
diff changeset
   103
        chunk_pos += (name -> make_pos(chunk.heading_length))
67272
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   104
      }
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   105
      for (tok <- chunk.tokens) {
67276
abac35ee3565 clarified positions;
wenzelm
parents: 67275
diff changeset
   106
        tokens += (tok.copy(source = tok.source.replace("\n", " ")) -> make_pos(tok.source.length))
67272
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   107
        advance_pos(tok)
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   108
      }
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   109
    }
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   110
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   111
    Isabelle_System.with_tmp_dir("bibtex")(tmp_dir =>
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   112
    {
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   113
      File.write(tmp_dir + Path.explode("root.bib"),
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   114
        tokens.iterator.map(p => p._1.source).mkString("", "\n", "\n"))
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   115
      File.write(tmp_dir + Path.explode("root.aux"),
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   116
        "\\bibstyle{plain}\n\\bibdata{root}\n\\citation{*}")
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   117
      Isabelle_System.bash("\"$ISABELLE_BIBTEX\" root", cwd = tmp_dir.file)
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   118
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   119
      val Error = """^(.*)---line (\d+) of file root.bib$""".r
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   120
      val Warning = """^Warning--(.+)$""".r
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   121
      val Warning_Line = """--line (\d+) of file root.bib$""".r
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   122
      val Warning_in_Chunk = """^Warning--(.+) in (.+)$""".r
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   123
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   124
      val log_file = tmp_dir + Path.explode("root.blg")
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   125
      val lines = if (log_file.is_file) Line.logical_lines(File.read(log_file)) else Nil
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   126
67301
e255c76db052 clarified signature;
wenzelm
parents: 67300
diff changeset
   127
      val (errors, warnings) =
69294
085f31ae902d more robust;
wenzelm
parents: 69259
diff changeset
   128
        if (lines.isEmpty) (Nil, Nil)
085f31ae902d more robust;
wenzelm
parents: 69259
diff changeset
   129
        else {
085f31ae902d more robust;
wenzelm
parents: 69259
diff changeset
   130
          lines.zip(lines.tail ::: List("")).flatMap(
085f31ae902d more robust;
wenzelm
parents: 69259
diff changeset
   131
            {
085f31ae902d more robust;
wenzelm
parents: 69259
diff changeset
   132
              case (Error(msg, Value.Int(l)), _) =>
085f31ae902d more robust;
wenzelm
parents: 69259
diff changeset
   133
                Some((true, (msg, get_line_pos(l))))
085f31ae902d more robust;
wenzelm
parents: 69259
diff changeset
   134
              case (Warning_in_Chunk(msg, name), _) if chunk_pos.isDefinedAt(name) =>
085f31ae902d more robust;
wenzelm
parents: 69259
diff changeset
   135
                Some((false, (Word.capitalize(msg + " in entry " + quote(name)), chunk_pos(name))))
085f31ae902d more robust;
wenzelm
parents: 69259
diff changeset
   136
              case (Warning(msg), Warning_Line(Value.Int(l))) =>
085f31ae902d more robust;
wenzelm
parents: 69259
diff changeset
   137
                Some((false, (Word.capitalize(msg), get_line_pos(l))))
085f31ae902d more robust;
wenzelm
parents: 69259
diff changeset
   138
              case (Warning(msg), _) =>
085f31ae902d more robust;
wenzelm
parents: 69259
diff changeset
   139
                Some((false, (Word.capitalize(msg), Position.none)))
085f31ae902d more robust;
wenzelm
parents: 69259
diff changeset
   140
              case _ => None
085f31ae902d more robust;
wenzelm
parents: 69259
diff changeset
   141
            }
085f31ae902d more robust;
wenzelm
parents: 69259
diff changeset
   142
          ).partition(_._1)
085f31ae902d more robust;
wenzelm
parents: 69259
diff changeset
   143
        }
67301
e255c76db052 clarified signature;
wenzelm
parents: 67300
diff changeset
   144
      (errors.map(_._2), warnings.map(_._2))
67272
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   145
    })
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   146
  }
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   147
72194
eef421b724c0 clarified names;
wenzelm
parents: 72193
diff changeset
   148
  object Check_Database extends Scala.Fun("bibtex_check_database")
67275
5e427586cb57 check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents: 67274
diff changeset
   149
  {
72756
72ac27ea12b2 more positions;
wenzelm
parents: 72729
diff changeset
   150
    val here = Scala_Project.here
72193
742d94015918 clarified signature;
wenzelm
parents: 70230
diff changeset
   151
    def apply(database: String): String =
742d94015918 clarified signature;
wenzelm
parents: 70230
diff changeset
   152
    {
742d94015918 clarified signature;
wenzelm
parents: 70230
diff changeset
   153
      import XML.Encode._
742d94015918 clarified signature;
wenzelm
parents: 70230
diff changeset
   154
      YXML.string_of_body(pair(list(pair(string, properties)), list(pair(string, properties)))(
742d94015918 clarified signature;
wenzelm
parents: 70230
diff changeset
   155
        check_database(database)))
742d94015918 clarified signature;
wenzelm
parents: 70230
diff changeset
   156
    }
67275
5e427586cb57 check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents: 67274
diff changeset
   157
  }
5e427586cb57 check bibtex database on ML side -- for semantic PIDE editing;
wenzelm
parents: 67274
diff changeset
   158
67272
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   159
c41a032d8386 check bibtex database: errors and warnings;
wenzelm
parents: 67257
diff changeset
   160
64828
e837f6bf653c clarified modules;
wenzelm
parents: 64824
diff changeset
   161
  /** document model **/
e837f6bf653c clarified modules;
wenzelm
parents: 64824
diff changeset
   162
67290
98b6cd12f963 implicit thy_load context for bibtex files;
wenzelm
parents: 67289
diff changeset
   163
  /* entries */
64828
e837f6bf653c clarified modules;
wenzelm
parents: 64824
diff changeset
   164
66150
c2e19b9e1398 tuned signature;
wenzelm
parents: 66118
diff changeset
   165
  def entries(text: String): List[Text.Info[String]] =
64828
e837f6bf653c clarified modules;
wenzelm
parents: 64824
diff changeset
   166
  {
64831
4792ee012e94 tuned signature;
wenzelm
parents: 64828
diff changeset
   167
    val result = new mutable.ListBuffer[Text.Info[String]]
64828
e837f6bf653c clarified modules;
wenzelm
parents: 64824
diff changeset
   168
    var offset = 0
e837f6bf653c clarified modules;
wenzelm
parents: 64824
diff changeset
   169
    for (chunk <- Bibtex.parse(text)) {
64831
4792ee012e94 tuned signature;
wenzelm
parents: 64828
diff changeset
   170
      val end_offset = offset + chunk.source.length
4792ee012e94 tuned signature;
wenzelm
parents: 64828
diff changeset
   171
      if (chunk.name != "" && !chunk.is_command)
4792ee012e94 tuned signature;
wenzelm
parents: 64828
diff changeset
   172
        result += Text.Info(Text.Range(offset, end_offset), chunk.name)
4792ee012e94 tuned signature;
wenzelm
parents: 64828
diff changeset
   173
      offset = end_offset
64828
e837f6bf653c clarified modules;
wenzelm
parents: 64824
diff changeset
   174
    }
e837f6bf653c clarified modules;
wenzelm
parents: 64824
diff changeset
   175
    result.toList
e837f6bf653c clarified modules;
wenzelm
parents: 64824
diff changeset
   176
  }
e837f6bf653c clarified modules;
wenzelm
parents: 64824
diff changeset
   177
66150
c2e19b9e1398 tuned signature;
wenzelm
parents: 66118
diff changeset
   178
  def entries_iterator[A, B <: Document.Model](models: Map[A, B])
c2e19b9e1398 tuned signature;
wenzelm
parents: 66118
diff changeset
   179
    : Iterator[Text.Info[(String, B)]] =
c2e19b9e1398 tuned signature;
wenzelm
parents: 66118
diff changeset
   180
  {
c2e19b9e1398 tuned signature;
wenzelm
parents: 66118
diff changeset
   181
    for {
c2e19b9e1398 tuned signature;
wenzelm
parents: 66118
diff changeset
   182
      (_, model) <- models.iterator
c2e19b9e1398 tuned signature;
wenzelm
parents: 66118
diff changeset
   183
      info <- model.bibtex_entries.iterator
c2e19b9e1398 tuned signature;
wenzelm
parents: 66118
diff changeset
   184
    } yield info.map((_, model))
c2e19b9e1398 tuned signature;
wenzelm
parents: 66118
diff changeset
   185
  }
c2e19b9e1398 tuned signature;
wenzelm
parents: 66118
diff changeset
   186
64828
e837f6bf653c clarified modules;
wenzelm
parents: 64824
diff changeset
   187
66152
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   188
  /* completion */
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   189
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   190
  def completion[A, B <: Document.Model](
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   191
    history: Completion.History, rendering: Rendering, caret: Text.Offset,
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   192
    models: Map[A, B]): Option[Completion.Result] =
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   193
  {
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   194
    for {
72729
83411077c37b clarified signature;
wenzelm
parents: 72652
diff changeset
   195
      Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption
66152
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   196
      name1 <- Completion.clean_name(name)
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   197
67014
e6a695d6a6b2 tuned signature;
wenzelm
parents: 66152
diff changeset
   198
      original <- rendering.model.get_text(r)
66152
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   199
      original1 <- Completion.clean_name(Library.perhaps_unquote(original))
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   200
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   201
      entries =
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   202
        (for {
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   203
          Text.Info(_, (entry, _)) <- entries_iterator(models)
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   204
          if entry.toLowerCase.containsSlice(name1.toLowerCase) && entry != original1
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   205
        } yield entry).toList
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   206
      if entries.nonEmpty
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   207
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   208
      items =
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   209
        entries.sorted.map({
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   210
          case entry =>
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   211
            val full_name = Long_Name.qualify(Markup.CITATION, entry)
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   212
            val description = List(entry, "(BibTeX entry)")
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   213
            val replacement = quote(entry)
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   214
          Completion.Item(r, original, full_name, description, replacement, 0, false)
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   215
        }).sorted(history.ordering).take(rendering.options.int("completion_limit"))
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   216
    } yield Completion.Result(r, original, false, items)
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   217
  }
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   218
18e1aba549f6 tuned signature;
wenzelm
parents: 66150
diff changeset
   219
64828
e837f6bf653c clarified modules;
wenzelm
parents: 64824
diff changeset
   220
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   221
  /** content **/
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   222
58529
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   223
  private val months = List(
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   224
    "jan",
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   225
    "feb",
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   226
    "mar",
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   227
    "apr",
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   228
    "may",
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   229
    "jun",
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   230
    "jul",
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   231
    "aug",
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   232
    "sep",
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   233
    "oct",
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   234
    "nov",
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   235
    "dec")
58529
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   236
  def is_month(s: String): Boolean = months.contains(s.toLowerCase)
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   237
58529
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   238
  private val commands = List("preamble", "string")
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   239
  def is_command(s: String): Boolean = commands.contains(s.toLowerCase)
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   240
58524
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   241
  sealed case class Entry(
58526
f05ccce3eca2 SideKick parser for bibtex entries;
wenzelm
parents: 58524
diff changeset
   242
    kind: String,
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   243
    required: List[String],
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   244
    optional_crossref: List[String],
58529
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   245
    optional_other: List[String])
58524
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   246
  {
70230
8ba266889dee more bibtex fields;
wenzelm
parents: 69367
diff changeset
   247
    val optional_standard: List[String] = List("url", "doi", "ee")
8ba266889dee more bibtex fields;
wenzelm
parents: 69367
diff changeset
   248
58533
dfbfc92118eb fields are case-insensitive;
wenzelm
parents: 58532
diff changeset
   249
    def is_required(s: String): Boolean = required.contains(s.toLowerCase)
58529
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   250
    def is_optional(s: String): Boolean =
70230
8ba266889dee more bibtex fields;
wenzelm
parents: 69367
diff changeset
   251
      optional_crossref.contains(s.toLowerCase) ||
8ba266889dee more bibtex fields;
wenzelm
parents: 69367
diff changeset
   252
      optional_other.contains(s.toLowerCase) ||
8ba266889dee more bibtex fields;
wenzelm
parents: 69367
diff changeset
   253
      optional_standard.contains(s.toLowerCase)
58529
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   254
70230
8ba266889dee more bibtex fields;
wenzelm
parents: 69367
diff changeset
   255
    def fields: List[String] =
8ba266889dee more bibtex fields;
wenzelm
parents: 69367
diff changeset
   256
      required ::: optional_crossref ::: optional_other ::: optional_standard
8ba266889dee more bibtex fields;
wenzelm
parents: 69367
diff changeset
   257
58524
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   258
    def template: String =
58526
f05ccce3eca2 SideKick parser for bibtex entries;
wenzelm
parents: 58524
diff changeset
   259
      "@" + kind + "{,\n" + fields.map(x => "  " + x + " = {},\n").mkString + "}\n"
58524
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   260
  }
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   261
66150
c2e19b9e1398 tuned signature;
wenzelm
parents: 66118
diff changeset
   262
  val known_entries: List[Entry] =
58524
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   263
    List(
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   264
      Entry("Article",
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   265
        List("author", "title"),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   266
        List("journal", "year"),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   267
        List("volume", "number", "pages", "month", "note")),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   268
      Entry("InProceedings",
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   269
        List("author", "title"),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   270
        List("booktitle", "year"),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   271
        List("editor", "volume", "number", "series", "pages", "month", "address",
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   272
          "organization", "publisher", "note")),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   273
      Entry("InCollection",
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   274
        List("author", "title", "booktitle"),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   275
        List("publisher", "year"),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   276
        List("editor", "volume", "number", "series", "type", "chapter", "pages",
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   277
          "edition", "month", "address", "note")),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   278
      Entry("InBook",
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   279
        List("author", "editor", "title", "chapter"),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   280
        List("publisher", "year"),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   281
        List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   282
      Entry("Proceedings",
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   283
        List("title", "year"),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   284
        List(),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   285
        List("booktitle", "editor", "volume", "number", "series", "address", "month",
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   286
          "organization", "publisher", "note")),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   287
      Entry("Book",
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   288
        List("author", "editor", "title"),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   289
        List("publisher", "year"),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   290
        List("volume", "number", "series", "address", "edition", "month", "note")),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   291
      Entry("Booklet",
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   292
        List("title"),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   293
        List(),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   294
        List("author", "howpublished", "address", "month", "year", "note")),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   295
      Entry("PhdThesis",
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   296
        List("author", "title", "school", "year"),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   297
        List(),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   298
        List("type", "address", "month", "note")),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   299
      Entry("MastersThesis",
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   300
        List("author", "title", "school", "year"),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   301
        List(),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   302
        List("type", "address", "month", "note")),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   303
      Entry("TechReport",
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   304
        List("author", "title", "institution", "year"),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   305
        List(),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   306
        List("type", "number", "address", "month", "note")),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   307
      Entry("Manual",
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   308
        List("title"),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   309
        List(),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   310
        List("author", "organization", "address", "edition", "month", "year", "note")),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   311
      Entry("Unpublished",
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   312
        List("author", "title", "note"),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   313
        List(),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   314
        List("month", "year")),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   315
      Entry("Misc",
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   316
        List(),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   317
        List(),
f805b366a497 context menu for bibtex entries;
wenzelm
parents: 58523
diff changeset
   318
        List("author", "title", "howpublished", "month", "year", "note")))
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   319
58529
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   320
  def get_entry(kind: String): Option[Entry] =
66150
c2e19b9e1398 tuned signature;
wenzelm
parents: 66118
diff changeset
   321
    known_entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase)
58529
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   322
58530
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   323
  def is_entry(kind: String): Boolean = get_entry(kind).isDefined
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   324
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   325
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   326
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   327
  /** tokens and chunks **/
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   328
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   329
  object Token
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   330
  {
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   331
    object Kind extends Enumeration
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   332
    {
58529
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   333
      val COMMAND = Value("command")
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   334
      val ENTRY = Value("entry")
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   335
      val KEYWORD = Value("keyword")
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   336
      val NAT = Value("natural number")
58529
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   337
      val STRING = Value("string")
58531
454962877285 more explicit chunk name;
wenzelm
parents: 58530
diff changeset
   338
      val NAME = Value("name")
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   339
      val IDENT = Value("identifier")
58535
4815429974fe more explicit comments;
wenzelm
parents: 58534
diff changeset
   340
      val SPACE = Value("white space")
4815429974fe more explicit comments;
wenzelm
parents: 58534
diff changeset
   341
      val COMMENT = Value("ignored text")
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   342
      val ERROR = Value("bad input")
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   343
    }
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   344
  }
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   345
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59319
diff changeset
   346
  sealed case class Token(kind: Token.Kind.Value, source: String)
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   347
  {
58530
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   348
    def is_kind: Boolean =
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   349
      kind == Token.Kind.COMMAND ||
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   350
      kind == Token.Kind.ENTRY ||
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   351
      kind == Token.Kind.IDENT
58531
454962877285 more explicit chunk name;
wenzelm
parents: 58530
diff changeset
   352
    def is_name: Boolean =
454962877285 more explicit chunk name;
wenzelm
parents: 58530
diff changeset
   353
      kind == Token.Kind.NAME ||
454962877285 more explicit chunk name;
wenzelm
parents: 58530
diff changeset
   354
      kind == Token.Kind.IDENT
58535
4815429974fe more explicit comments;
wenzelm
parents: 58534
diff changeset
   355
    def is_ignored: Boolean =
4815429974fe more explicit comments;
wenzelm
parents: 58534
diff changeset
   356
      kind == Token.Kind.SPACE ||
4815429974fe more explicit comments;
wenzelm
parents: 58534
diff changeset
   357
      kind == Token.Kind.COMMENT
67276
abac35ee3565 clarified positions;
wenzelm
parents: 67275
diff changeset
   358
    def is_malformed: Boolean =
abac35ee3565 clarified positions;
wenzelm
parents: 67275
diff changeset
   359
      kind == Token.Kind.ERROR
abac35ee3565 clarified positions;
wenzelm
parents: 67275
diff changeset
   360
    def is_open: Boolean =
abac35ee3565 clarified positions;
wenzelm
parents: 67275
diff changeset
   361
      kind == Token.Kind.KEYWORD && (source == "{" || source == "(")
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   362
  }
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   363
58530
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   364
  case class Chunk(kind: String, tokens: List[Token])
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   365
  {
58529
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   366
    val source = tokens.map(_.source).mkString
58526
f05ccce3eca2 SideKick parser for bibtex entries;
wenzelm
parents: 58524
diff changeset
   367
58530
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   368
    private val content: Option[List[Token]] =
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   369
      tokens match {
59319
wenzelm
parents: 58609
diff changeset
   370
        case Token(Token.Kind.KEYWORD, "@") :: body if body.nonEmpty =>
58529
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   371
          (body.init.filterNot(_.is_ignored), body.last) match {
58530
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   372
            case (tok :: Token(Token.Kind.KEYWORD, "{") :: toks, Token(Token.Kind.KEYWORD, "}"))
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   373
            if tok.is_kind => Some(toks)
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   374
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   375
            case (tok :: Token(Token.Kind.KEYWORD, "(") :: toks, Token(Token.Kind.KEYWORD, ")"))
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   376
            if tok.is_kind => Some(toks)
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   377
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   378
            case _ => None
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   379
          }
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   380
        case _ => None
58526
f05ccce3eca2 SideKick parser for bibtex entries;
wenzelm
parents: 58524
diff changeset
   381
      }
f05ccce3eca2 SideKick parser for bibtex entries;
wenzelm
parents: 58524
diff changeset
   382
f05ccce3eca2 SideKick parser for bibtex entries;
wenzelm
parents: 58524
diff changeset
   383
    def name: String =
58530
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   384
      content match {
58531
454962877285 more explicit chunk name;
wenzelm
parents: 58530
diff changeset
   385
        case Some(tok :: _) if tok.is_name => tok.source
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   386
        case _ => ""
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   387
      }
58530
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   388
67276
abac35ee3565 clarified positions;
wenzelm
parents: 67275
diff changeset
   389
    def heading_length: Int =
abac35ee3565 clarified positions;
wenzelm
parents: 67275
diff changeset
   390
      if (name == "") 1
abac35ee3565 clarified positions;
wenzelm
parents: 67275
diff changeset
   391
      else (0 /: tokens.takeWhile(tok => !tok.is_open)){ case (n, tok) => n + tok.source.length }
abac35ee3565 clarified positions;
wenzelm
parents: 67275
diff changeset
   392
58530
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   393
    def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   394
    def is_malformed: Boolean = kind == "" || tokens.exists(_.is_malformed)
58543
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 58538
diff changeset
   395
    def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined
9c1389befa56 maintain Document_Model.bibtex_entries;
wenzelm
parents: 58538
diff changeset
   396
    def is_entry: Boolean = Bibtex.is_entry(kind) && name != "" && content.isDefined
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   397
  }
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   398
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   399
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   400
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   401
  /** parsing **/
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   402
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   403
  // context of partial line-oriented scans
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   404
  abstract class Line_Context
58589
d9350ec0937e tuned signature;
wenzelm
parents: 58544
diff changeset
   405
  case object Ignored extends Line_Context
58590
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   406
  case object At extends Line_Context
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   407
  case class Item_Start(kind: String) extends Line_Context
58591
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   408
  case class Item_Open(kind: String, end: String) extends Line_Context
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   409
  case class Item(kind: String, end: String, delim: Delimited) extends Line_Context
58590
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   410
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   411
  case class Delimited(quoted: Boolean, depth: Int)
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   412
  val Closed = Delimited(false, 0)
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   413
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   414
  private def token(kind: Token.Kind.Value)(source: String): Token = Token(kind, source)
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   415
  private def keyword(source: String): Token = Token(Token.Kind.KEYWORD, source)
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   416
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   417
68224
1f7308050349 prefer HTTPS;
wenzelm
parents: 67301
diff changeset
   418
  // See also https://ctan.org/tex-archive/biblio/bibtex/base/bibtex.web
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   419
  // module @<Scan for and process a \.{.bib} command or database entry@>.
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   420
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   421
  object Parsers extends RegexParsers
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   422
  {
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   423
    /* white space and comments */
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   424
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   425
    override val whiteSpace = "".r
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   426
58535
4815429974fe more explicit comments;
wenzelm
parents: 58534
diff changeset
   427
    private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.SPACE)
58590
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   428
    private val spaces = rep(space)
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   429
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   430
58535
4815429974fe more explicit comments;
wenzelm
parents: 58534
diff changeset
   431
    /* ignored text */
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   432
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   433
    private val ignored: Parser[Chunk] =
58609
d0cb70d66bc1 removed pointless regexp flags;
wenzelm
parents: 58596
diff changeset
   434
      rep1("""(?i)([^@]+|@[ \t]*comment)""".r) ^^ {
58535
4815429974fe more explicit comments;
wenzelm
parents: 58534
diff changeset
   435
        case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) }
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   436
58536
402a8e8107a7 more total chunk_line: recovery via ignored_line;
wenzelm
parents: 58535
diff changeset
   437
    private def ignored_line: Parser[(Chunk, Line_Context)] =
58589
d9350ec0937e tuned signature;
wenzelm
parents: 58544
diff changeset
   438
      ignored ^^ { case a => (a, Ignored) }
58536
402a8e8107a7 more total chunk_line: recovery via ignored_line;
wenzelm
parents: 58535
diff changeset
   439
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   440
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   441
    /* delimited string: outermost "..." or {...} and body with balanced {...} */
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   442
58534
573ce5ad13bc clarified nesting of delimiters;
wenzelm
parents: 58533
diff changeset
   443
    // see also bibtex.web: scan_a_field_token_and_eat_white, scan_balanced_braces
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   444
    private def delimited_depth(delim: Delimited): Parser[(String, Delimited)] =
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   445
      new Parser[(String, Delimited)]
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   446
      {
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   447
        require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0)
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   448
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   449
        def apply(in: Input) =
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   450
        {
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   451
          val start = in.offset
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   452
          val end = in.source.length
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   453
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   454
          var i = start
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   455
          var q = delim.quoted
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   456
          var d = delim.depth
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   457
          var finished = false
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   458
          while (!finished && i < end) {
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   459
            val c = in.source.charAt(i)
58534
573ce5ad13bc clarified nesting of delimiters;
wenzelm
parents: 58533
diff changeset
   460
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   461
            if (c == '"' && d == 0) { i += 1; d = 1; q = true }
58532
af2fc25662b6 clarified nesting of delimiters;
wenzelm
parents: 58531
diff changeset
   462
            else if (c == '"' && d == 1 && q) {
af2fc25662b6 clarified nesting of delimiters;
wenzelm
parents: 58531
diff changeset
   463
              i += 1; d = 0; q = false; finished = true
af2fc25662b6 clarified nesting of delimiters;
wenzelm
parents: 58531
diff changeset
   464
            }
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   465
            else if (c == '{') { i += 1; d += 1 }
58534
573ce5ad13bc clarified nesting of delimiters;
wenzelm
parents: 58533
diff changeset
   466
            else if (c == '}') {
573ce5ad13bc clarified nesting of delimiters;
wenzelm
parents: 58533
diff changeset
   467
              if (d == 1 && !q || d > 1) { i += 1; d -= 1; if (d == 0) finished = true }
573ce5ad13bc clarified nesting of delimiters;
wenzelm
parents: 58533
diff changeset
   468
              else {i = start; finished = true }
58532
af2fc25662b6 clarified nesting of delimiters;
wenzelm
parents: 58531
diff changeset
   469
            }
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   470
            else if (d > 0) i += 1
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   471
            else finished = true
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   472
          }
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   473
          if (i == start) Failure("bad input", in)
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   474
          else {
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   475
            val s = in.source.subSequence(start, i).toString
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   476
            Success((s, Delimited(q, d)), in.drop(i - start))
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   477
          }
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   478
        }
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   479
      }.named("delimited_depth")
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   480
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   481
    private def delimited: Parser[Token] =
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   482
      delimited_depth(Closed) ^?
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   483
        { case (s, delim) if delim == Closed => Token(Token.Kind.STRING, s) }
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   484
58534
573ce5ad13bc clarified nesting of delimiters;
wenzelm
parents: 58533
diff changeset
   485
    private def recover_delimited: Parser[Token] =
58609
d0cb70d66bc1 removed pointless regexp flags;
wenzelm
parents: 58596
diff changeset
   486
      """["{][^@]*""".r ^^ token(Token.Kind.ERROR)
58534
573ce5ad13bc clarified nesting of delimiters;
wenzelm
parents: 58533
diff changeset
   487
58590
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   488
    def delimited_line(ctxt: Item): Parser[(Chunk, Line_Context)] =
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   489
      delimited_depth(ctxt.delim) ^^ { case (s, delim1) =>
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   490
        (Chunk(ctxt.kind, List(Token(Token.Kind.STRING, s))), ctxt.copy(delim = delim1)) } |
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   491
      recover_delimited ^^ { case a => (Chunk(ctxt.kind, List(a)), Ignored) }
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   492
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   493
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   494
    /* other tokens */
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   495
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   496
    private val at = "@" ^^ keyword
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   497
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   498
    private val nat = "[0-9]+".r ^^ token(Token.Kind.NAT)
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   499
58591
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   500
    private val name = """[\x21-\x7f&&[^"#%'(),={}]]+""".r ^^ token(Token.Kind.NAME)
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   501
58529
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   502
    private val identifier =
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   503
      """[\x21-\x7f&&[^"#%'(),={}0-9]][\x21-\x7f&&[^"#%'(),={}]]*""".r
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   504
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   505
    private val ident = identifier ^^ token(Token.Kind.IDENT)
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   506
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   507
    val other_token = "[=#,]".r ^^ keyword | (nat | (ident | space))
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   508
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   509
58591
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   510
    /* body */
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   511
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   512
    private val body =
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   513
      delimited | (recover_delimited | other_token)
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   514
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   515
    private def body_line(ctxt: Item) =
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   516
      if (ctxt.delim.depth > 0)
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   517
        delimited_line(ctxt)
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   518
      else
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   519
        delimited_line(ctxt) |
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   520
        other_token ^^ { case a => (Chunk(ctxt.kind, List(a)), ctxt) } |
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   521
        ctxt.end ^^ { case a => (Chunk(ctxt.kind, List(keyword(a))), Ignored) }
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   522
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   523
58530
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   524
    /* items: command or entry */
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   525
58530
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   526
    private val item_kind =
58529
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   527
      identifier ^^ { case a =>
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   528
        val kind =
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   529
          if (is_command(a)) Token.Kind.COMMAND
58530
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   530
          else if (is_entry(a)) Token.Kind.ENTRY
58529
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   531
          else Token.Kind.IDENT
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   532
        Token(kind, a)
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   533
      }
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 58528
diff changeset
   534
58591
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   535
    private val item_begin =
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   536
      "{" ^^ { case a => ("}", keyword(a)) } |
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   537
      "(" ^^ { case a => (")", keyword(a)) }
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   538
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   539
    private def item_name(kind: String) =
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   540
      kind.toLowerCase match {
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   541
        case "preamble" => failure("")
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   542
        case "string" => identifier ^^ token(Token.Kind.NAME)
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   543
        case _ => name
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   544
      }
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   545
58531
454962877285 more explicit chunk name;
wenzelm
parents: 58530
diff changeset
   546
    private val item_start =
58590
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   547
      at ~ spaces ~ item_kind ~ spaces ^^
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   548
        { case a ~ b ~ c ~ d => (c.source, List(a) ::: b ::: List(c) ::: d) }
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   549
58530
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   550
    private val item: Parser[Chunk] =
58591
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   551
      (item_start ~ item_begin ~ spaces) into
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   552
        { case (kind, a) ~ ((end, b)) ~ c =>
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   553
            opt(item_name(kind)) ~ rep(body) ~ opt(end ^^ keyword) ^^ {
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   554
              case d ~ e ~ f => Chunk(kind, a ::: List(b) ::: c ::: d.toList ::: e ::: f.toList) } }
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   555
58530
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   556
    private val recover_item: Parser[Chunk] =
58609
d0cb70d66bc1 removed pointless regexp flags;
wenzelm
parents: 58596
diff changeset
   557
      at ~ "[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) }
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   558
58591
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   559
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   560
    /* chunks */
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   561
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   562
    val chunk: Parser[Chunk] = ignored | (item | recover_item)
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   563
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   564
    def chunk_line(ctxt: Line_Context): Parser[(Chunk, Line_Context)] =
58530
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   565
    {
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   566
      ctxt match {
58589
d9350ec0937e tuned signature;
wenzelm
parents: 58544
diff changeset
   567
        case Ignored =>
58538
299b82d12d53 proper treatment of @comment (amending 402a8e8107a7);
wenzelm
parents: 58536
diff changeset
   568
          ignored_line |
58590
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   569
          at ^^ { case a => (Chunk("", List(a)), At) }
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   570
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   571
        case At =>
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   572
          space ^^ { case a => (Chunk("", List(a)), ctxt) } |
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   573
          item_kind ^^ { case a => (Chunk(a.source, List(a)), Item_Start(a.source)) } |
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   574
          recover_item ^^ { case a => (a, Ignored) } |
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   575
          ignored_line
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   576
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   577
        case Item_Start(kind) =>
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   578
          space ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
58591
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   579
          item_begin ^^ { case (end, a) => (Chunk(kind, List(a)), Item_Open(kind, end)) } |
58596
877c5ecee253 more total parser;
wenzelm
parents: 58591
diff changeset
   580
          recover_item ^^ { case a => (a, Ignored) } |
58590
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   581
          ignored_line
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   582
58591
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   583
        case Item_Open(kind, end) =>
58590
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   584
          space ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
58591
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   585
          item_name(kind) ^^ { case a => (Chunk(kind, List(a)), Item(kind, end, Closed)) } |
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   586
          body_line(Item(kind, end, Closed)) |
58590
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   587
          ignored_line
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   588
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   589
        case item_ctxt: Item =>
58591
3c1a8c1c6b3b more accurate item name, depending on kind;
wenzelm
parents: 58590
diff changeset
   590
          body_line(item_ctxt) |
58590
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   591
          ignored_line
472b9fbcc7f0 back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;
wenzelm
parents: 58589
diff changeset
   592
58530
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   593
        case _ => failure("")
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   594
      }
7ee248f19ca9 clarified Chunk -- avoid ooddities;
wenzelm
parents: 58529
diff changeset
   595
    }
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   596
  }
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   597
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   598
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   599
  /* parse */
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   600
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   601
  def parse(input: CharSequence): List[Chunk] =
64824
330ec9bc4b75 tuned signature;
wenzelm
parents: 60215
diff changeset
   602
    Parsers.parseAll(Parsers.rep(Parsers.chunk), Scan.char_reader(input)) match {
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   603
      case Parsers.Success(result, _) => result
58526
f05ccce3eca2 SideKick parser for bibtex entries;
wenzelm
parents: 58524
diff changeset
   604
      case _ => error("Unexpected failure to parse input:\n" + input.toString)
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   605
    }
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   606
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   607
  def parse_line(input: CharSequence, context: Line_Context): (List[Chunk], Line_Context) =
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   608
  {
64824
330ec9bc4b75 tuned signature;
wenzelm
parents: 60215
diff changeset
   609
    var in: Reader[Char] = Scan.char_reader(input)
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   610
    val chunks = new mutable.ListBuffer[Chunk]
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   611
    var ctxt = context
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   612
    while (!in.atEnd) {
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   613
      Parsers.parse(Parsers.chunk_line(ctxt), in) match {
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59319
diff changeset
   614
        case Parsers.Success((x, c), rest) => chunks += x; ctxt = c; in = rest
58528
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   615
        case Parsers.NoSuccess(_, rest) =>
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   616
          error("Unepected failure to parse input:\n" + rest.source.toString)
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   617
      }
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   618
    }
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   619
    (chunks.toList, ctxt)
7d6b8f8893e8 more explicit item kind;
wenzelm
parents: 58527
diff changeset
   620
  }
67243
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   621
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   622
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   623
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   624
  /** HTML output **/
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   625
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   626
  private val output_styles =
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   627
    List(
67257
5035b6754fca clarified signature;
wenzelm
parents: 67256
diff changeset
   628
      "" -> "html-n",
67243
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   629
      "plain" -> "html-n",
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   630
      "alpha" -> "html-a",
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   631
      "named" -> "html-n",
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   632
      "paragraph" -> "html-n",
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   633
      "unsort" -> "html-u",
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   634
      "unsortlist" -> "html-u")
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   635
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   636
  def html_output(bib: List[Path],
67256
ce7d856680d1 proper title;
wenzelm
parents: 67251
diff changeset
   637
    title: String = "Bibliography",
67248
68177abb2988 isabelle.preview presents bibtex database files as well;
wenzelm
parents: 67243
diff changeset
   638
    body: Boolean = false,
67243
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   639
    citations: List[String] = List("*"),
67257
5035b6754fca clarified signature;
wenzelm
parents: 67256
diff changeset
   640
    style: String = "",
67243
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   641
    chronological: Boolean = false): String =
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   642
  {
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   643
    Isabelle_System.with_tmp_dir("bibtex")(tmp_dir =>
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   644
    {
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   645
      /* database files */
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   646
69367
34b7550b66c7 tuned signature;
wenzelm
parents: 69366
diff changeset
   647
      val bib_files = bib.map(_.drop_ext)
67243
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   648
      val bib_names =
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   649
      {
69366
b6dacf6eabe3 clarified signature;
wenzelm
parents: 69294
diff changeset
   650
        val names0 = bib_files.map(_.file_name)
67243
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   651
        if (Library.duplicates(names0).isEmpty) names0
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   652
        else names0.zipWithIndex.map({ case (name, i) => (i + 1).toString + "-" + name })
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   653
      }
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   654
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   655
      for ((a, b) <- bib_files zip bib_names) {
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   656
        File.copy(a.ext("bib"), tmp_dir + Path.basic(b).ext("bib"))
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   657
      }
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   658
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   659
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   660
      /* style file */
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   661
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   662
      val bst =
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   663
        output_styles.toMap.get(style) match {
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   664
          case Some(base) => base + (if (chronological) "c" else "") + ".bst"
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   665
          case None =>
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   666
            error("Bad style for bibtex HTML output: " + quote(style) +
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   667
              "\n(expected: " + commas_quote(output_styles.map(_._1)) + ")")
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   668
        }
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   669
      File.copy(Path.explode("$BIB2XHTML_HOME/bst") + Path.explode(bst), tmp_dir)
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   670
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   671
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   672
      /* result */
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   673
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   674
      val in_file = Path.explode("bib.aux")
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   675
      val out_file = Path.explode("bib.html")
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   676
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   677
      File.write(tmp_dir + in_file,
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   678
        bib_names.mkString("\\bibdata{", ",", "}\n") +
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   679
        citations.map(cite => "\\citation{" + cite + "}\n").mkString)
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   680
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   681
      Isabelle_System.bash(
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   682
        "\"$BIB2XHTML_HOME/main/bib2xhtml.pl\" -B \"$ISABELLE_BIBTEX\"" +
67257
5035b6754fca clarified signature;
wenzelm
parents: 67256
diff changeset
   683
          " -u -s " + Bash.string(proper_string(style) getOrElse "empty") +
5035b6754fca clarified signature;
wenzelm
parents: 67256
diff changeset
   684
          (if (chronological) " -c" else "") +
67256
ce7d856680d1 proper title;
wenzelm
parents: 67251
diff changeset
   685
          (if (title != "") " -h " + Bash.string(title) + " " else "") +
ce7d856680d1 proper title;
wenzelm
parents: 67251
diff changeset
   686
          " " + File.bash_path(in_file) + " " + File.bash_path(out_file),
67243
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   687
        cwd = tmp_dir.file).check
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   688
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   689
      val html = File.read(tmp_dir + out_file)
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   690
67248
68177abb2988 isabelle.preview presents bibtex database files as well;
wenzelm
parents: 67243
diff changeset
   691
      if (body) {
68177abb2988 isabelle.preview presents bibtex database files as well;
wenzelm
parents: 67243
diff changeset
   692
        cat_lines(
68177abb2988 isabelle.preview presents bibtex database files as well;
wenzelm
parents: 67243
diff changeset
   693
          split_lines(html).
68177abb2988 isabelle.preview presents bibtex database files as well;
wenzelm
parents: 67243
diff changeset
   694
            dropWhile(line => !line.startsWith("<!-- BEGIN BIBLIOGRAPHY")).reverse.
68177abb2988 isabelle.preview presents bibtex database files as well;
wenzelm
parents: 67243
diff changeset
   695
            dropWhile(line => !line.startsWith("<!-- END BIBLIOGRAPHY")).reverse)
68177abb2988 isabelle.preview presents bibtex database files as well;
wenzelm
parents: 67243
diff changeset
   696
      }
68177abb2988 isabelle.preview presents bibtex database files as well;
wenzelm
parents: 67243
diff changeset
   697
      else html
67243
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   698
    })
6a93aaa3ed36 bibtex HTML output via external tool;
wenzelm
parents: 67203
diff changeset
   699
  }
58523
937c479e62fe some support for bibtex files;
wenzelm
parents:
diff changeset
   700
}