# HG changeset patch
# User wenzelm
# Date 1664631772 -7200
# Node ID f3b23f4eaaac8b990f3a20d8d4c3eac3304d5435
# Parent  fc19de122712ecbdd98a1e999e538c0cfe6d7b6f
clarified signature, to support external tools like "isabelle narration";

diff -r fc19de122712 -r f3b23f4eaaac src/Pure/PIDE/rendering.scala
--- 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 =