clarified spell-checking (see also 30233285270a);
authorwenzelm
Sun Mar 24 17:53:46 2019 +0100 (3 months ago)
changeset 699681a400b14fd3a
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
     1.1 --- a/etc/options	Sun Mar 24 17:45:00 2019 +0100
     1.2 +++ b/etc/options	Sun Mar 24 17:53:46 2019 +0100
     1.3 @@ -242,7 +242,7 @@
     1.4  public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment"
     1.5    -- "included markup elements for spell-checker (separated by commas)"
     1.6  
     1.7 -public option spell_checker_exclude : string = "no_words,antiquoted"
     1.8 +public option spell_checker_exclude : string = "antiquoted,raw_text"
     1.9    -- "excluded markup elements for spell-checker (separated by commas)"
    1.10  
    1.11  
     2.1 --- a/src/Pure/General/comment.ML	Sun Mar 24 17:45:00 2019 +0100
     2.2 +++ b/src/Pure/General/comment.ML	Sun Mar 24 17:53:46 2019 +0100
     2.3 @@ -34,7 +34,7 @@
     2.4        markups = [Markup.language_text true, Markup.raw_text]}),
     2.5     (Latex,
     2.6       {symbol = Symbol.latex, blanks = false,
     2.7 -      markups = [Markup.language_latex true, Markup.no_words, Markup.raw_text]}),
     2.8 +      markups = [Markup.language_latex true, Markup.raw_text]}),
     2.9     (Marker,
    2.10       {symbol = Symbol.marker, blanks = false,
    2.11        markups = [Markup.language_document_marker]})];
     3.1 --- a/src/Pure/PIDE/markup.ML	Sun Mar 24 17:45:00 2019 +0100
     3.2 +++ b/src/Pure/PIDE/markup.ML	Sun Mar 24 17:53:46 2019 +0100
     3.3 @@ -78,7 +78,6 @@
     3.4    val fbreakN: string val fbreak: T
     3.5    val itemN: string val item: T
     3.6    val wordsN: string val words: T
     3.7 -  val no_wordsN: string val no_words: T
     3.8    val hiddenN: string val hidden: T
     3.9    val deleteN: string val delete: T
    3.10    val system_optionN: string
    3.11 @@ -433,7 +432,6 @@
    3.12  (* text properties *)
    3.13  
    3.14  val (wordsN, words) = markup_elem "words";
    3.15 -val (no_wordsN, no_words) = markup_elem "no_words";
    3.16  
    3.17  val (hiddenN, hidden) = markup_elem "hidden";
    3.18  
     4.1 --- a/src/Tools/Haskell/Haskell.thy	Sun Mar 24 17:45:00 2019 +0100
     4.2 +++ b/src/Tools/Haskell/Haskell.thy	Sun Mar 24 17:53:46 2019 +0100
     4.3 @@ -327,7 +327,7 @@
     4.4    markupN, consistentN, unbreakableN, indentN, widthN,
     4.5    blockN, block, breakN, break, fbreakN, fbreak, itemN, item,
     4.6  
     4.7 -  wordsN, words, no_wordsN, no_words,
     4.8 +  wordsN, words,
     4.9  
    4.10    tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
    4.11    numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string,
    4.12 @@ -510,9 +510,6 @@
    4.13  wordsN :: String; words :: T
    4.14  (wordsN, words) = markup_elem \<open>Markup.wordsN\<close>
    4.15  
    4.16 -no_wordsN :: String; no_words :: T
    4.17 -(no_wordsN, no_words) = markup_elem \<open>Markup.no_wordsN\<close>
    4.18 -
    4.19  
    4.20  {- inner syntax -}
    4.21