--- a/src/Tools/jEdit/src/spell_checker.scala Tue Dec 20 18:11:42 2016 +0100
+++ b/src/Tools/jEdit/src/spell_checker.scala Tue Dec 20 21:35:56 2016 +0100
@@ -61,7 +61,7 @@
result.toList
}
- def current_word(text_area: TextArea, rendering: Rendering, range: Text.Range)
+ def current_word(text_area: TextArea, rendering: JEdit_Rendering, range: Text.Range)
: Option[Text.Info[String]] =
{
for {
@@ -75,7 +75,7 @@
/** completion **/
- def completion(text_area: TextArea, explicit: Boolean, rendering: Rendering)
+ def completion(text_area: TextArea, explicit: Boolean, rendering: JEdit_Rendering)
: Option[Completion.Result] =
{
for {