equal
deleted
inserted
replaced
70 |
70 |
71 def refresh() |
71 def refresh() |
72 { |
72 { |
73 Swing_Thread.require() |
73 Swing_Thread.require() |
74 |
74 |
|
75 val font = new Font(current_font_family, Font.PLAIN, current_font_size) |
|
76 getPainter.setFont(font) |
|
77 getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias"))) |
|
78 getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size)) |
|
79 |
75 if (getWidth > 0) { |
80 if (getWidth > 0) { |
76 val font = new Font(current_font_family, Font.PLAIN, current_font_size) |
|
77 getPainter.setFont(font) |
|
78 getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias"))) |
|
79 getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size)) |
|
80 |
|
81 val font_metrics = getPainter.getFontMetrics(font) |
81 val font_metrics = getPainter.getFontMetrics(font) |
82 val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20 |
82 val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20 |
83 |
83 |
84 val base_snapshot = current_base_snapshot |
84 val base_snapshot = current_base_snapshot |
85 val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics)) |
85 val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics)) |