# HG changeset patch
# User wenzelm
# Date 1556798759 -7200
# Node ID c03f381fd37303196a8890b57131e116b2b09d54
# Parent  ce9134bdc1d4f1e5307f58312b71dfe809b2471f
clarified PIDE markup;

diff -r ce9134bdc1d4 -r c03f381fd373 etc/options
--- a/etc/options	Thu May 02 11:43:56 2019 +0200
+++ b/etc/options	Thu May 02 14:05:59 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 ce9134bdc1d4 -r c03f381fd373 src/Pure/General/comment.ML
--- a/src/Pure/General/comment.ML	Thu May 02 11:43:56 2019 +0200
+++ b/src/Pure/General/comment.ML	Thu May 02 14:05:59 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 ce9134bdc1d4 -r c03f381fd373 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu May 02 11:43:56 2019 +0200
+++ b/src/Pure/PIDE/markup.ML	Thu May 02 14:05:59 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;