--- 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)"
--- 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;
--- 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;
--- 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"
}