diff -r cb07791d86b8 -r f2d641e856ac src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 26 15:16:37 2020 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 26 15:18:09 2020 +0100
@@ -76,7 +76,7 @@
 
     getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
     getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
-    get_background().map(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) })
+    get_background().foreach(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) })
     getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor"))
     getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor"))
     getGutter.setFont(jEdit.getFontProperty("view.gutter.font"))
@@ -95,7 +95,7 @@
       val results = current_base_results
       val formatted_body = Pretty.formatted(current_body, margin = margin, metric = metric)
 
-      future_refresh.map(_.cancel)
+      future_refresh.foreach(_.cancel)
       future_refresh =
         Some(Future.fork {
           val (text, rendering) =