# HG changeset patch
# User wenzelm
# Date 1516890065 -3600
# Node ID 30233285270acbc71503d9aa50e9a2992561f38b
# Parent  ceb324e34c149b36266022068b92c9029b920eb0
more markup: disable spell-checker for raw latex;

diff -r ceb324e34c14 -r 30233285270a etc/options
--- a/etc/options	Thu Jan 25 14:13:55 2018 +0100
+++ b/etc/options	Thu Jan 25 15:21:05 2018 +0100
@@ -217,7 +217,7 @@
 public option spell_checker_include : string = "words,comment,inner_comment,ML_comment,SML_comment"
   -- "included markup elements for spell-checker (separated by commas)"
 
-public option spell_checker_exclude : string = "antiquoted"
+public option spell_checker_exclude : string = "no_words,antiquoted"
   -- "excluded markup elements for spell-checker (separated by commas)"
 
 
diff -r ceb324e34c14 -r 30233285270a src/Pure/General/comment.ML
--- a/src/Pure/General/comment.ML	Thu Jan 25 14:13:55 2018 +0100
+++ b/src/Pure/General/comment.ML	Thu Jan 25 15:21:05 2018 +0100
@@ -7,7 +7,7 @@
 signature COMMENT =
 sig
   datatype kind = Comment | Cancel | Latex
-  val markup: kind -> Markup.T
+  val markups: kind -> Markup.T list
   val scan_comment: (kind * Symbol_Pos.T list) scanner
   val scan_cancel: (kind * Symbol_Pos.T list) scanner
   val scan_latex: (kind * Symbol_Pos.T list) scanner
@@ -23,13 +23,19 @@
 datatype kind = Comment | Cancel | Latex;
 
 val kinds =
-  [(Comment, {symbol = Symbol.comment, blanks = true, markup = Markup.language_document true}),
-   (Cancel, {symbol = Symbol.cancel, blanks = false, markup = Markup.language_text true}),
-   (Latex, {symbol = Symbol.latex, blanks = false, markup = Markup.language_latex true})];
+  [(Comment,
+     {symbol = Symbol.comment, blanks = true,
+      markups = [Markup.language_document true]}),
+   (Cancel,
+     {symbol = Symbol.cancel, blanks = false,
+      markups = [Markup.language_text true]}),
+   (Latex,
+     {symbol = Symbol.latex, blanks = false,
+      markups = [Markup.language_latex true, Markup.no_words]})];
 
 val get_kind = the o AList.lookup (op =) kinds;
 val print_kind = quote o #symbol o get_kind;
-val markup = #markup o get_kind;
+val markups = #markups o get_kind;
 
 fun is_symbol sym = exists (fn (_, {symbol, ...}) => symbol = sym) kinds;
 
diff -r ceb324e34c14 -r 30233285270a src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Jan 25 14:13:55 2018 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu Jan 25 15:21:05 2018 +0100
@@ -71,6 +71,7 @@
   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 system_optionN: string
   val sessionN: string
@@ -393,6 +394,7 @@
 (* 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 ceb324e34c14 -r 30233285270a src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Jan 25 14:13:55 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Thu Jan 25 15:21:05 2018 +0100
@@ -147,7 +147,7 @@
       val pos = #1 (Symbol_Pos.range syms);
       val _ =
         comment |> Option.app (fn kind =>
-          Context_Position.reports ctxt [(pos, Comment.markup kind), (pos, Markup.cartouche)]);
+          Context_Position.reports ctxt (map (pair pos) (Markup.cartouche :: Comment.markups kind)));
       val _ = output_symbols_comment ctxt {antiq = false} (comment, syms);
     in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);