# HG changeset patch # User wenzelm # Date 1553446426 -3600 # Node ID 1a400b14fd3a7e8c8760825db9fb4fb4263c7c08 # Parent 8a9d0d894ec0339a20d098a9c63052f170f74124 clarified spell-checking (see also 30233285270a); diff -r 8a9d0d894ec0 -r 1a400b14fd3a etc/options --- 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)" diff -r 8a9d0d894ec0 -r 1a400b14fd3a src/Pure/General/comment.ML --- 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]})]; diff -r 8a9d0d894ec0 -r 1a400b14fd3a src/Pure/PIDE/markup.ML --- 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"; diff -r 8a9d0d894ec0 -r 1a400b14fd3a src/Tools/Haskell/Haskell.thy --- 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 \Markup.wordsN\ -no_wordsN :: String; no_words :: T -(no_wordsN, no_words) = markup_elem \Markup.no_wordsN\ - {- inner syntax -}