clarified spell-checking (see also 30233285270a);
authorwenzelm
Sun, 24 Mar 2019 17:53:46 +0100
changeset 69968 1a400b14fd3a
parent 69967 8a9d0d894ec0
child 69969 c211db89f916
clarified spell-checking (see also 30233285270a);
etc/options
src/Pure/General/comment.ML
src/Pure/PIDE/markup.ML
src/Tools/Haskell/Haskell.thy
--- a/etc/options	Sun Mar 24 17:45:00 2019 +0100
+++ b/etc/options	Sun Mar 24 17:53:46 2019 +0100
@@ -242,7 +242,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 = "no_words,antiquoted"
+public option spell_checker_exclude : string = "antiquoted,raw_text"
   -- "excluded markup elements for spell-checker (separated by commas)"
 
 
--- a/src/Pure/General/comment.ML	Sun Mar 24 17:45:00 2019 +0100
+++ b/src/Pure/General/comment.ML	Sun Mar 24 17:53:46 2019 +0100
@@ -34,7 +34,7 @@
       markups = [Markup.language_text true, Markup.raw_text]}),
    (Latex,
      {symbol = Symbol.latex, blanks = false,
-      markups = [Markup.language_latex true, Markup.no_words, Markup.raw_text]}),
+      markups = [Markup.language_latex true, Markup.raw_text]}),
    (Marker,
      {symbol = Symbol.marker, blanks = false,
       markups = [Markup.language_document_marker]})];
--- a/src/Pure/PIDE/markup.ML	Sun Mar 24 17:45:00 2019 +0100
+++ b/src/Pure/PIDE/markup.ML	Sun Mar 24 17:53:46 2019 +0100
@@ -78,7 +78,6 @@
   val fbreakN: string val fbreak: T
   val itemN: string val item: T
   val wordsN: string val words: T
-  val no_wordsN: string val no_words: T
   val hiddenN: string val hidden: T
   val deleteN: string val delete: T
   val system_optionN: string
@@ -433,7 +432,6 @@
 (* text properties *)
 
 val (wordsN, words) = markup_elem "words";
-val (no_wordsN, no_words) = markup_elem "no_words";
 
 val (hiddenN, hidden) = markup_elem "hidden";
 
--- a/src/Tools/Haskell/Haskell.thy	Sun Mar 24 17:45:00 2019 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Sun Mar 24 17:53:46 2019 +0100
@@ -327,7 +327,7 @@
   markupN, consistentN, unbreakableN, indentN, widthN,
   blockN, block, breakN, break, fbreakN, fbreak, itemN, item,
 
-  wordsN, words, no_wordsN, no_words,
+  wordsN, words,
 
   tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
   numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string,
@@ -510,9 +510,6 @@
 wordsN :: String; words :: T
 (wordsN, words) = markup_elem \<open>Markup.wordsN\<close>
 
-no_wordsN :: String; no_words :: T
-(no_wordsN, no_words) = markup_elem \<open>Markup.no_wordsN\<close>
-
 
 {- inner syntax -}