more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
authorwenzelm
Tue Jan 09 20:15:36 2018 +0100 (17 months ago)
changeset 67395b39d596b77ce
parent 67394 b591933d39ec
child 67396 172a02125bfa
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
NEWS
etc/options
src/Doc/JEdit/JEdit.thy
src/Pure/PIDE/rendering.scala
src/Tools/VSCode/src/vscode_spell_checker.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/NEWS	Tue Jan 09 20:03:14 2018 +0100
     1.2 +++ b/NEWS	Tue Jan 09 20:15:36 2018 +0100
     1.3 @@ -51,6 +51,10 @@
     1.4  
     1.5  *** Isabelle/jEdit Prover IDE ***
     1.6  
     1.7 +* System options "spell_checker_include" and "spell_checker_exclude"
     1.8 +supersede former "spell_checker_elements" to determine regions of text
     1.9 +that are subject to spell-checking. Minor INCOMPATIBILITY.
    1.10 +
    1.11  * PIDE markup for session ROOT files: allows to complete session names,
    1.12  follow links to theories and document files etc.
    1.13  
     2.1 --- a/etc/options	Tue Jan 09 20:03:14 2018 +0100
     2.2 +++ b/etc/options	Tue Jan 09 20:15:36 2018 +0100
     2.3 @@ -214,8 +214,11 @@
     2.4  public option spell_checker_dictionary : string = "en"
     2.5    -- "spell-checker dictionary name"
     2.6  
     2.7 -public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment"
     2.8 -  -- "relevant markup elements for spell-checker, separated by commas"
     2.9 +public option spell_checker_include : string = "words,comment,inner_comment,ML_comment,SML_comment"
    2.10 +  -- "included markup elements for spell-checker (separated by commas)"
    2.11 +
    2.12 +public option spell_checker_exclude : string = "antiquoted"
    2.13 +  -- "excluded markup elements for spell-checker (separated by commas)"
    2.14  
    2.15  
    2.16  section "Secure Shell"
     3.1 --- a/src/Doc/JEdit/JEdit.thy	Tue Jan 09 20:03:14 2018 +0100
     3.2 +++ b/src/Doc/JEdit/JEdit.thy	Tue Jan 09 20:15:36 2018 +0100
     3.3 @@ -1673,9 +1673,13 @@
     3.4    permanent dictionary updates is stored in the directory @{path
     3.5    "$ISABELLE_HOME_USER/dictionaries"}, in a separate file for each dictionary.
     3.6  
     3.7 -  \<^item> @{system_option_def spell_checker_elements} specifies a comma-separated
     3.8 +  \<^item> @{system_option_def spell_checker_include} specifies a comma-separated
     3.9    list of markup elements that delimit words in the source that is subject to
    3.10    spell-checking, including various forms of comments.
    3.11 +
    3.12 +  \<^item> @{system_option_def spell_checker_exclude} specifies a comma-separated
    3.13 +  list of markup elements that disable spell-checking (e.g.\ in nested
    3.14 +  antiquotations).
    3.15  \<close>
    3.16  
    3.17  
     4.1 --- a/src/Pure/PIDE/rendering.scala	Tue Jan 09 20:03:14 2018 +0100
     4.2 +++ b/src/Pure/PIDE/rendering.scala	Tue Jan 09 20:15:36 2018 +0100
     4.3 @@ -355,17 +355,30 @@
     4.4  
     4.5    /* spell checker */
     4.6  
     4.7 +  private lazy val spell_checker_include =
     4.8 +    Markup.Elements(space_explode(',', options.string("spell_checker_include")): _*)
     4.9 +
    4.10    private lazy val spell_checker_elements =
    4.11 -    Markup.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
    4.12 +    spell_checker_include ++
    4.13 +      Markup.Elements(space_explode(',', options.string("spell_checker_exclude")): _*)
    4.14  
    4.15 -  def spell_checker_ranges(range: Text.Range): List[Text.Range] =
    4.16 -    snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range)
    4.17 +  def spell_checker(range: Text.Range): List[Text.Info[Text.Range]] =
    4.18 +  {
    4.19 +    val result =
    4.20 +      snapshot.select(range, spell_checker_elements, _ =>
    4.21 +        {
    4.22 +          case info =>
    4.23 +            Some(
    4.24 +              if (spell_checker_include(info.info.name))
    4.25 +                Some(snapshot.convert(info.range))
    4.26 +              else None)
    4.27 +        })
    4.28 +    for (Text.Info(range, Some(range1)) <- result)
    4.29 +      yield Text.Info(range, range1)
    4.30 +  }
    4.31  
    4.32    def spell_checker_point(range: Text.Range): Option[Text.Range] =
    4.33 -    snapshot.select(range, spell_checker_elements, _ =>
    4.34 -      {
    4.35 -        case info => Some(snapshot.convert(info.range))
    4.36 -      }).headOption.map(_.info)
    4.37 +    spell_checker(range).headOption.map(_.info)
    4.38  
    4.39  
    4.40    /* text background */
     5.1 --- a/src/Tools/VSCode/src/vscode_spell_checker.scala	Tue Jan 09 20:03:14 2018 +0100
     5.2 +++ b/src/Tools/VSCode/src/vscode_spell_checker.scala	Tue Jan 09 20:15:36 2018 +0100
     5.3 @@ -18,9 +18,9 @@
     5.4      val ranges =
     5.5        (for {
     5.6          spell_checker <- rendering.resources.spell_checker.get.iterator
     5.7 -        spell_range <- rendering.spell_checker_ranges(model.content.text_range).iterator
     5.8 -        text <- model.get_text(spell_range).iterator
     5.9 -        info <- spell_checker.marked_words(spell_range.start, text).iterator
    5.10 +        spell <- rendering.spell_checker(model.content.text_range).iterator
    5.11 +        text <- model.get_text(spell.range).iterator
    5.12 +        info <- spell_checker.marked_words(spell.range.start, text).iterator
    5.13        } yield info.range).toList
    5.14      Document_Model.Decoration.ranges("spell_checker", ranges)
    5.15    }
     6.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Tue Jan 09 20:03:14 2018 +0100
     6.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Tue Jan 09 20:15:36 2018 +0100
     6.3 @@ -344,9 +344,9 @@
     6.4              // spell checker
     6.5              for {
     6.6                spell_checker <- PIDE.plugin.spell_checker.get
     6.7 -              spell_range <- rendering.spell_checker_ranges(line_range)
     6.8 -              text <- JEdit_Lib.get_text(buffer, spell_range)
     6.9 -              info <- spell_checker.marked_words(spell_range.start, text)
    6.10 +              spell <- rendering.spell_checker(line_range)
    6.11 +              text <- JEdit_Lib.get_text(buffer, spell.range)
    6.12 +              info <- spell_checker.marked_words(spell.range.start, text)
    6.13                r <- JEdit_Lib.gfx_range(text_area, info.range)
    6.14              } {
    6.15                gfx.setColor(rendering.spell_checker_color)