Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Thu, 26 Nov 2020 15:18:09 +0100
changeset 72720 f2d641e856ac
parent 72719 cb07791d86b8
child 72721 79f5e843e5ec
tuned;
src/Tools/jEdit/src/pretty_text_area.scala file | annotate | diff | comparison | revisions 
--- 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) =
isabelle