--- a/src/Pure/PIDE/rendering.scala Fri Sep 30 21:03:58 2022 +0200
+++ b/src/Pure/PIDE/rendering.scala Sat Oct 01 15:42:52 2022 +0200
@@ -398,12 +398,14 @@
/* spell checker */
- private lazy val spell_checker_include =
+ lazy val spell_checker_include: Markup.Elements =
Markup.Elements(space_explode(',', options.string("spell_checker_include")): _*)
- private lazy val spell_checker_elements =
- spell_checker_include ++
- Markup.Elements(space_explode(',', options.string("spell_checker_exclude")): _*)
+ lazy val spell_checker_exclude: Markup.Elements =
+ Markup.Elements(space_explode(',', options.string("spell_checker_exclude")): _*)
+
+ lazy val spell_checker_elements: Markup.Elements =
+ spell_checker_include ++ spell_checker_exclude
def spell_checker(range: Text.Range): List[Text.Info[Text.Range]] = {
val result =