77 } |
77 } |
78 |
78 |
79 private val builder = new DocumentBuilderImpl(ucontext, rcontext) |
79 private val builder = new DocumentBuilderImpl(ucontext, rcontext) |
80 |
80 |
81 |
81 |
82 /* physical document */ |
82 /* document template with style sheets */ |
83 |
83 |
84 private def template(font_size: Int): String = |
84 private val template_head = |
85 { |
|
86 """<?xml version="1.0" encoding="utf-8"?> |
85 """<?xml version="1.0" encoding="utf-8"?> |
87 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" |
86 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" |
88 "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
87 "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
89 <html xmlns="http://www.w3.org/1999/xhtml"> |
88 <html xmlns="http://www.w3.org/1999/xhtml"> |
90 <head> |
89 <head> |
91 <style media="all" type="text/css"> |
90 <style media="all" type="text/css"> |
92 """ + |
91 """ + |
93 system.try_read("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" + |
92 system.try_read("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" + |
94 system.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" + |
93 system.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" |
95 "body { font-family: " + system.font_family + "; font-size: " + raw_px(font_size) + "px }" + |
94 |
|
95 private val template_tail = |
96 """ |
96 """ |
97 </style> |
97 </style> |
98 </head> |
98 </head> |
99 <body/> |
99 <body/> |
100 </html> |
100 </html> |
101 """ |
101 """ |
102 } |
102 |
|
103 private def template(font_size: Int): String = |
|
104 template_head + |
|
105 "body { font-family: " + system.font_family + "; font-size: " + raw_px(font_size) + "px }" + |
|
106 template_tail |
|
107 |
|
108 |
|
109 /* physical document */ |
103 |
110 |
104 private class Doc |
111 private class Doc |
105 { |
112 { |
106 private var current_font_size: Int = 0 |
113 private var current_font_size: Int = 0 |
107 private var current_font_metrics: FontMetrics = null |
114 private var current_font_metrics: FontMetrics = null |