--- a/etc/options Sat Mar 11 11:24:02 2023 +0100
+++ b/etc/options Sat Mar 11 11:31:58 2023 +0100
@@ -291,16 +291,16 @@
section "Spell Checker"
-public option spell_checker : bool = true for content
+public option spell_checker : bool = true
-- "enable spell-checker for prose words within document text, comments etc."
-public option spell_checker_dictionary : string = "en" for content
+public option spell_checker_dictionary : string = "en"
-- "spell-checker dictionary name"
-public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment" for content
+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 = "document_marker,antiquoted,raw_text" for content
+public option spell_checker_exclude : string = "document_marker,antiquoted,raw_text"
-- "excluded markup elements for spell-checker (separated by commas)"
--- a/src/Pure/System/options.scala Sat Mar 11 11:24:02 2023 +0100
+++ b/src/Pure/System/options.scala Sat Mar 11 11:31:58 2023 +0100
@@ -91,7 +91,11 @@
def unknown: Boolean = typ == Unknown
def has_tag(tag: String): Boolean = tags.contains(tag)
- def is_exported: Boolean = !has_tag(TAG_CONNECTION)
+
+ def session_content: Boolean =
+ has_tag(TAG_CONTENT) ||
+ has_tag(TAG_DOCUMENT) ||
+ has_tag(TAG_UPDATE)
}
--- a/src/Pure/Tools/build_process.scala Sat Mar 11 11:24:02 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Sat Mar 11 11:31:58 2023 +0100
@@ -923,7 +923,7 @@
final def start_build(): Unit = synchronized_database {
for (db <- _database) {
Build_Process.Data.start_build(db, build_uuid, build_context.ml_platform,
- store.options.make_prefs(Options.init(prefs = ""), filter = _.is_exported))
+ store.options.make_prefs(Options.init(prefs = ""), filter = _.session_content))
}
}