more markup: disable spell-checker for raw latex;
authorwenzelm
Thu Jan 25 15:21:05 2018 +0100 (17 months ago)
changeset 6750630233285270a
parent 67505 ceb324e34c14
child 67507 5db077cfe1b2
more markup: disable spell-checker for raw latex;
etc/options
src/Pure/General/comment.ML
src/Pure/PIDE/markup.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/etc/options	Thu Jan 25 14:13:55 2018 +0100
     1.2 +++ b/etc/options	Thu Jan 25 15:21:05 2018 +0100
     1.3 @@ -217,7 +217,7 @@
     1.4  public option spell_checker_include : string = "words,comment,inner_comment,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 = "antiquoted"
     1.8 +public option spell_checker_exclude : string = "no_words,antiquoted"
     1.9    -- "excluded markup elements for spell-checker (separated by commas)"
    1.10  
    1.11  
     2.1 --- a/src/Pure/General/comment.ML	Thu Jan 25 14:13:55 2018 +0100
     2.2 +++ b/src/Pure/General/comment.ML	Thu Jan 25 15:21:05 2018 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  signature COMMENT =
     2.5  sig
     2.6    datatype kind = Comment | Cancel | Latex
     2.7 -  val markup: kind -> Markup.T
     2.8 +  val markups: kind -> Markup.T list
     2.9    val scan_comment: (kind * Symbol_Pos.T list) scanner
    2.10    val scan_cancel: (kind * Symbol_Pos.T list) scanner
    2.11    val scan_latex: (kind * Symbol_Pos.T list) scanner
    2.12 @@ -23,13 +23,19 @@
    2.13  datatype kind = Comment | Cancel | Latex;
    2.14  
    2.15  val kinds =
    2.16 -  [(Comment, {symbol = Symbol.comment, blanks = true, markup = Markup.language_document true}),
    2.17 -   (Cancel, {symbol = Symbol.cancel, blanks = false, markup = Markup.language_text true}),
    2.18 -   (Latex, {symbol = Symbol.latex, blanks = false, markup = Markup.language_latex true})];
    2.19 +  [(Comment,
    2.20 +     {symbol = Symbol.comment, blanks = true,
    2.21 +      markups = [Markup.language_document true]}),
    2.22 +   (Cancel,
    2.23 +     {symbol = Symbol.cancel, blanks = false,
    2.24 +      markups = [Markup.language_text true]}),
    2.25 +   (Latex,
    2.26 +     {symbol = Symbol.latex, blanks = false,
    2.27 +      markups = [Markup.language_latex true, Markup.no_words]})];
    2.28  
    2.29  val get_kind = the o AList.lookup (op =) kinds;
    2.30  val print_kind = quote o #symbol o get_kind;
    2.31 -val markup = #markup o get_kind;
    2.32 +val markups = #markups o get_kind;
    2.33  
    2.34  fun is_symbol sym = exists (fn (_, {symbol, ...}) => symbol = sym) kinds;
    2.35  
     3.1 --- a/src/Pure/PIDE/markup.ML	Thu Jan 25 14:13:55 2018 +0100
     3.2 +++ b/src/Pure/PIDE/markup.ML	Thu Jan 25 15:21:05 2018 +0100
     3.3 @@ -71,6 +71,7 @@
     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 system_optionN: string
    3.10    val sessionN: string
    3.11 @@ -393,6 +394,7 @@
    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/Pure/Thy/thy_output.ML	Thu Jan 25 14:13:55 2018 +0100
     4.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Jan 25 15:21:05 2018 +0100
     4.3 @@ -147,7 +147,7 @@
     4.4        val pos = #1 (Symbol_Pos.range syms);
     4.5        val _ =
     4.6          comment |> Option.app (fn kind =>
     4.7 -          Context_Position.reports ctxt [(pos, Comment.markup kind), (pos, Markup.cartouche)]);
     4.8 +          Context_Position.reports ctxt (map (pair pos) (Markup.cartouche :: Comment.markups kind)));
     4.9        val _ = output_symbols_comment ctxt {antiq = false} (comment, syms);
    4.10      in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);
    4.11