equal
deleted
inserted
replaced
74 } |
74 } |
75 getPainter.setFoldLineStyle(fold_line_style) |
75 getPainter.setFoldLineStyle(fold_line_style) |
76 |
76 |
77 getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor")) |
77 getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor")) |
78 getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor")) |
78 getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor")) |
79 get_background().map(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) }) |
79 get_background().foreach(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) }) |
80 getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor")) |
80 getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor")) |
81 getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor")) |
81 getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor")) |
82 getGutter.setFont(jEdit.getFontProperty("view.gutter.font")) |
82 getGutter.setFont(jEdit.getFontProperty("view.gutter.font")) |
83 getGutter.setBorder(0, |
83 getGutter.setBorder(0, |
84 jEdit.getColorProperty("view.gutter.focusBorderColor"), |
84 jEdit.getColorProperty("view.gutter.focusBorderColor"), |
93 |
93 |
94 val snapshot = current_base_snapshot |
94 val snapshot = current_base_snapshot |
95 val results = current_base_results |
95 val results = current_base_results |
96 val formatted_body = Pretty.formatted(current_body, margin = margin, metric = metric) |
96 val formatted_body = Pretty.formatted(current_body, margin = margin, metric = metric) |
97 |
97 |
98 future_refresh.map(_.cancel) |
98 future_refresh.foreach(_.cancel) |
99 future_refresh = |
99 future_refresh = |
100 Some(Future.fork { |
100 Some(Future.fork { |
101 val (text, rendering) = |
101 val (text, rendering) = |
102 try { JEdit_Rendering.text(snapshot, formatted_body, results = results) } |
102 try { JEdit_Rendering.text(snapshot, formatted_body, results = results) } |
103 catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn } |
103 catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn } |