# HG changeset patch
# User paulson
# Date 1556808057 -3600
# Node ID 778366b0f519b6ce0f33269566389d714b301e5d
# Parent  cdbc8d92c3491f0306d2d725de478e4c6fa3bd25# Parent  d19266b7465f5c8f726fa35bacade903c4d929c1
merged

diff -r d19266b7465f -r 778366b0f519 etc/options
--- a/etc/options	Thu May 02 15:40:36 2019 +0100
+++ b/etc/options	Thu May 02 15:40:57 2019 +0100
@@ -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 d19266b7465f -r 778366b0f519 src/Pure/General/comment.ML
--- a/src/Pure/General/comment.ML	Thu May 02 15:40:36 2019 +0100
+++ b/src/Pure/General/comment.ML	Thu May 02 15:40:57 2019 +0100
@@ -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 d19266b7465f -r 778366b0f519 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu May 02 15:40:36 2019 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu May 02 15:40:57 2019 +0100
@@ -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 d19266b7465f -r 778366b0f519 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Thu May 02 15:40:36 2019 +0100
+++ b/src/Pure/Thy/bibtex.scala	Thu May 02 15:40:57 2019 +0100
@@ -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"
   }