# HG changeset patch
# User wenzelm
# Date 1556800999 -7200
# Node ID cdbc8d92c3491f0306d2d725de478e4c6fa3bd25
# Parent  2d5b122aa0ff43bb6d1692d6c07f3ba1348b5711# Parent  8ba266889deee6bd8a0818f00128f444ba784a0e
merged

diff -r 2d5b122aa0ff -r cdbc8d92c349 etc/options
--- a/etc/options	Thu May 02 12:58:32 2019 +0100
+++ b/etc/options	Thu May 02 14:43:19 2019 +0200
@@ -246,7 +246,7 @@
 public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment"
   -- "included markup elements for spell-checker (separated by commas)"
 
-public option spell_checker_exclude : string = "antiquoted,raw_text"
+public option spell_checker_exclude : string = "document_marker,antiquoted,raw_text"
   -- "excluded markup elements for spell-checker (separated by commas)"
 
 
diff -r 2d5b122aa0ff -r cdbc8d92c349 src/Pure/General/comment.ML
--- a/src/Pure/General/comment.ML	Thu May 02 12:58:32 2019 +0100
+++ b/src/Pure/General/comment.ML	Thu May 02 14:43:19 2019 +0200
@@ -37,7 +37,7 @@
       markups = [Markup.language_latex true, Markup.raw_text]}),
    (Marker,
      {symbol = Symbol.marker, blanks = false,
-      markups = [Markup.language_document_marker]})];
+      markups = [Markup.language_document_marker, Markup.document_marker]})];
 
 val get_kind = the o AList.lookup (op =) kinds;
 val print_kind = quote o #symbol o get_kind;
diff -r 2d5b122aa0ff -r cdbc8d92c349 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu May 02 12:58:32 2019 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu May 02 14:43:19 2019 +0200
@@ -132,6 +132,7 @@
   val plain_textN: string val plain_text: T
   val paragraphN: string val paragraph: T
   val text_foldN: string val text_fold: T
+  val document_markerN: string val document_marker: T
   val document_tagN: string val document_tag: string -> T
   val markdown_paragraphN: string val markdown_paragraph: T
   val markdown_itemN: string val markdown_item: T
@@ -521,6 +522,7 @@
 val (paragraphN, paragraph) = markup_elem "paragraph";
 val (text_foldN, text_fold) = markup_elem "text_fold";
 
+val (document_markerN, document_marker) = markup_elem "document_marker";
 val (document_tagN, document_tag) = markup_string "document_tag" nameN;
 
 
diff -r 2d5b122aa0ff -r cdbc8d92c349 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Thu May 02 12:58:32 2019 +0100
+++ b/src/Pure/Thy/bibtex.scala	Thu May 02 14:43:19 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"
   }