# HG changeset patch
# User wenzelm
# Date 1556800282 -7200
# Node ID 8ba266889deee6bd8a0818f00128f444ba784a0e
# Parent  c03f381fd37303196a8890b57131e116b2b09d54
more bibtex fields;

diff -r c03f381fd373 -r 8ba266889dee src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Thu May 02 14:05:59 2019 +0200
+++ b/src/Pure/Thy/bibtex.scala	Thu May 02 14:31:22 2019 +0200
@@ -240,11 +240,17 @@
     optional_crossref: List[String],
     optional_other: List[String])
   {
+    val optional_standard: List[String] = List("url", "doi", "ee")
+
     def is_required(s: String): Boolean = required.contains(s.toLowerCase)
     def is_optional(s: String): Boolean =
-      optional_crossref.contains(s.toLowerCase) || optional_other.contains(s.toLowerCase)
+      optional_crossref.contains(s.toLowerCase) ||
+      optional_other.contains(s.toLowerCase) ||
+      optional_standard.contains(s.toLowerCase)
 
-    def fields: List[String] = required ::: optional_crossref ::: optional_other
+    def fields: List[String] =
+      required ::: optional_crossref ::: optional_other ::: optional_standard
+
     def template: String =
       "@" + kind + "{,\n" + fields.map(x => "  " + x + " = {},\n").mkString + "}\n"
   }