src/Pure/Tools/bibtex.scala
changeset 58524 f805b366a497
parent 58523 937c479e62fe
child 58526 f05ccce3eca2
equal deleted inserted replaced
58523:937c479e62fe 58524:f805b366a497
    29     "nov",
    29     "nov",
    30     "dec")
    30     "dec")
    31 
    31 
    32   val commands = List("preamble", "string")
    32   val commands = List("preamble", "string")
    33 
    33 
    34   sealed case class Entry_Type(
    34   sealed case class Entry(
       
    35     name: String,
    35     required: List[String],
    36     required: List[String],
    36     optional_crossref: List[String],
    37     optional_crossref: List[String],
    37     optional: List[String])
    38     optional: List[String])
    38 
    39   {
    39   val entries =
    40     def fields: List[String] = required ::: optional_crossref ::: optional
    40     Map[String, Entry_Type](
    41     def template: String =
    41       "Article" ->
    42       "@" + name + "{,\n" + fields.map(x => "  " + x + " = {},\n").mkString + "}\n"
    42         Entry_Type(
    43   }
    43           List("author", "title"),
    44 
    44           List("journal", "year"),
    45   val entries: List[Entry] =
    45           List("volume", "number", "pages", "month", "note")),
    46     List(
    46       "InProceedings" ->
    47       Entry("Article",
    47         Entry_Type(
    48         List("author", "title"),
    48           List("author", "title"),
    49         List("journal", "year"),
    49           List("booktitle", "year"),
    50         List("volume", "number", "pages", "month", "note")),
    50           List("editor", "volume", "number", "series", "pages", "month", "address",
    51       Entry("InProceedings",
    51             "organization", "publisher", "note")),
    52         List("author", "title"),
    52       "InCollection" ->
    53         List("booktitle", "year"),
    53         Entry_Type(
    54         List("editor", "volume", "number", "series", "pages", "month", "address",
    54           List("author", "title", "booktitle"),
    55           "organization", "publisher", "note")),
    55           List("publisher", "year"),
    56       Entry("InCollection",
    56           List("editor", "volume", "number", "series", "type", "chapter", "pages",
    57         List("author", "title", "booktitle"),
    57             "edition", "month", "address", "note")),
    58         List("publisher", "year"),
    58       "InBook" ->
    59         List("editor", "volume", "number", "series", "type", "chapter", "pages",
    59         Entry_Type(
    60           "edition", "month", "address", "note")),
    60          List("author", "editor", "title", "chapter"),
    61       Entry("InBook",
    61          List("publisher", "year"),
    62         List("author", "editor", "title", "chapter"),
    62          List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")),
    63         List("publisher", "year"),
    63       "Proceedings" ->
    64         List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")),
    64         Entry_Type(
    65       Entry("Proceedings",
    65           List("title", "year"),
    66         List("title", "year"),
    66           List(),
    67         List(),
    67           List("booktitle", "editor", "volume", "number", "series", "address", "month",
    68         List("booktitle", "editor", "volume", "number", "series", "address", "month",
    68             "organization", "publisher", "note")),
    69           "organization", "publisher", "note")),
    69       "Book" ->
    70       Entry("Book",
    70         Entry_Type(
    71         List("author", "editor", "title"),
    71           List("author", "editor", "title"),
    72         List("publisher", "year"),
    72           List("publisher", "year"),
    73         List("volume", "number", "series", "address", "edition", "month", "note")),
    73           List("volume", "number", "series", "address", "edition", "month", "note")),
    74       Entry("Booklet",
    74       "Booklet" ->
    75         List("title"),
    75         Entry_Type(
    76         List(),
    76           List("title"),
    77         List("author", "howpublished", "address", "month", "year", "note")),
    77           List(),
    78       Entry("PhdThesis",
    78           List("author", "howpublished", "address", "month", "year", "note")),
    79         List("author", "title", "school", "year"),
    79       "PhdThesis" ->
    80         List(),
    80         Entry_Type(
    81         List("type", "address", "month", "note")),
    81           List("author", "title", "school", "year"),
    82       Entry("MastersThesis",
    82           List(),
    83         List("author", "title", "school", "year"),
    83           List("type", "address", "month", "note")),
    84         List(),
    84       "MastersThesis" ->
    85         List("type", "address", "month", "note")),
    85         Entry_Type(
    86       Entry("TechReport",
    86           List("author", "title", "school", "year"),
    87         List("author", "title", "institution", "year"),
    87           List(),
    88         List(),
    88           List("type", "address", "month", "note")),
    89         List("type", "number", "address", "month", "note")),
    89       "TechReport" ->
    90       Entry("Manual",
    90         Entry_Type(
    91         List("title"),
    91           List("author", "title", "institution", "year"),
    92         List(),
    92           List(),
    93         List("author", "organization", "address", "edition", "month", "year", "note")),
    93           List("type", "number", "address", "month", "note")),
    94       Entry("Unpublished",
    94       "Manual" ->
    95         List("author", "title", "note"),
    95         Entry_Type(
    96         List(),
    96           List("title"),
    97         List("month", "year")),
    97           List(),
    98       Entry("Misc",
    98           List("author", "organization", "address", "edition", "month", "year", "note")),
    99         List(),
    99       "Unpublished" ->
   100         List(),
   100         Entry_Type(
   101         List("author", "title", "howpublished", "month", "year", "note")))
   101           List("author", "title", "note"),
       
   102           List(),
       
   103           List("month", "year")),
       
   104       "Misc" ->
       
   105         Entry_Type(
       
   106           List(),
       
   107           List(),
       
   108           List("author", "title", "howpublished", "month", "year", "note")))
       
   109 
   102 
   110 
   103 
   111 
   104 
   112   /** tokens and chunks **/
   105   /** tokens and chunks **/
   113 
   106