equal
deleted
inserted
replaced
103 |
103 |
104 private class Doc |
104 private class Doc |
105 { |
105 { |
106 var current_font_size: Int = 0 |
106 var current_font_size: Int = 0 |
107 var current_font_metrics: FontMetrics = null |
107 var current_font_metrics: FontMetrics = null |
108 var current_margin: Int = 0 |
|
109 var current_body: List[XML.Tree] = Nil |
108 var current_body: List[XML.Tree] = Nil |
110 var current_DOM: org.w3c.dom.Document = null |
109 var current_DOM: org.w3c.dom.Document = null |
111 |
110 |
112 def resize(font_size: Int) |
111 def resize(font_size: Int) |
113 { |
112 { |
114 if (font_size != current_font_size || current_font_metrics == null) { |
113 if (font_size != current_font_size || current_font_metrics == null) { |
115 Swing_Thread.now { |
114 Swing_Thread.now { |
116 current_font_size = font_size |
115 current_font_size = font_size |
117 current_font_metrics = |
116 current_font_metrics = |
118 getFontMetrics(system.get_font(lobo_px(raw_px(font_size)))) |
117 getFontMetrics(system.get_font(lobo_px(raw_px(font_size)))) |
119 current_margin = |
|
120 (getWidth() / (current_font_metrics.charWidth(Symbol.spc) max 1) - 4) max 20 |
|
121 } |
118 } |
122 current_DOM = |
119 current_DOM = |
123 builder.parse( |
120 builder.parse( |
124 new InputSourceImpl(new StringReader(template(font_size)), "http://localhost")) |
121 new InputSourceImpl(new StringReader(template(font_size)), "http://localhost")) |
125 render(current_body) |
122 render(current_body) |
127 } |
124 } |
128 |
125 |
129 def render(body: List[XML.Tree]) |
126 def render(body: List[XML.Tree]) |
130 { |
127 { |
131 current_body = body |
128 current_body = body |
|
129 val margin = (getWidth() / (current_font_metrics.charWidth(Symbol.spc) max 1) - 4) max 20 |
132 val html_body = |
130 val html_body = |
133 current_body.flatMap(div => |
131 current_body.flatMap(div => |
134 Pretty.formatted(List(div), current_margin, |
132 Pretty.formatted(List(div), margin, |
135 Pretty.font_metric(current_font_metrics)) |
133 Pretty.font_metric(current_font_metrics)) |
136 .map(t => XML.elem(HTML.PRE, HTML.spans(t)))) |
134 .map(t => XML.elem(HTML.PRE, HTML.spans(t)))) |
137 |
135 |
138 val node = XML.document_node(current_DOM, XML.elem(HTML.BODY, html_body)) |
136 val node = XML.document_node(current_DOM, XML.elem(HTML.BODY, html_body)) |
139 current_DOM.removeChild(current_DOM.getLastChild()) |
137 current_DOM.removeChild(current_DOM.getLastChild()) |