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) |
75 if (getWidth > 0) { |
76 getPainter.setFont(font) |
76 val font = new Font(current_font_family, Font.PLAIN, current_font_size) |
77 getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias"))) |
77 getPainter.setFont(font) |
78 getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size)) |
78 getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias"))) |
|
79 getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size)) |
79 |
80 |
80 val font_metrics = getPainter.getFontMetrics(font) |
81 val font_metrics = getPainter.getFontMetrics(font) |
81 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 |
82 |
83 |
83 val base_snapshot = current_base_snapshot |
84 val base_snapshot = current_base_snapshot |
84 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)) |
85 |
86 |
86 future_rendering.map(_.cancel(true)) |
87 future_rendering.map(_.cancel(true)) |
87 future_rendering = Some(default_thread_pool.submit(() => |
88 future_rendering = Some(default_thread_pool.submit(() => |
88 { |
89 { |
89 val (text, rendering) = Pretty_Text_Area.text_rendering(base_snapshot, formatted_body) |
90 val (text, rendering) = Pretty_Text_Area.text_rendering(base_snapshot, formatted_body) |
90 Simple_Thread.interrupted_exception() |
91 Simple_Thread.interrupted_exception() |
91 |
92 |
92 Swing_Thread.later { |
93 Swing_Thread.later { |
93 current_rendering = rendering |
94 current_rendering = rendering |
94 |
95 |
95 try { |
96 try { |
96 getBuffer.beginCompoundEdit |
97 getBuffer.beginCompoundEdit |
97 getBuffer.setReadOnly(false) |
98 getBuffer.setReadOnly(false) |
98 setText(text) |
99 setText(text) |
99 setCaretPosition(0) |
100 setCaretPosition(0) |
100 getBuffer.setReadOnly(true) |
101 getBuffer.setReadOnly(true) |
|
102 } |
|
103 finally { |
|
104 getBuffer.endCompoundEdit |
|
105 } |
101 } |
106 } |
102 finally { |
107 })) |
103 getBuffer.endCompoundEdit |
108 } |
104 } |
|
105 } |
|
106 })) |
|
107 } |
109 } |
108 |
110 |
109 def resize(font_family: String, font_size: Int) |
111 def resize(font_family: String, font_size: Int) |
110 { |
112 { |
111 Swing_Thread.require() |
113 Swing_Thread.require() |