65 |
65 |
66 private val div_elements = |
66 private val div_elements = |
67 Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name, |
67 Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name, |
68 HTML.descr.name) |
68 HTML.descr.name) |
69 |
69 |
70 private def html_div(html: XML.Body): Boolean = |
70 def make_html_body(xml: XML.Body): XML.Body = |
71 html exists { |
71 { |
72 case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body) |
72 def html_div(html: XML.Body): Boolean = |
73 case XML.Text(_) => false |
73 html exists { |
74 } |
74 case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body) |
75 |
75 case XML.Text(_) => false |
76 private def html_class(c: String, html: XML.Body): XML.Tree = |
76 } |
77 if (html.forall(_ == XML.no_text)) XML.no_text |
77 |
78 else if (html_div(html)) HTML.div(c, html) |
78 def html_class(c: String, html: XML.Body): XML.Tree = |
79 else HTML.span(c, html) |
79 if (html.forall(_ == XML.no_text)) XML.no_text |
80 |
80 else if (html_div(html)) HTML.div(c, html) |
81 private def html_body(xml: XML.Body): XML.Body = |
81 else HTML.span(c, html) |
82 xml map { |
82 |
83 case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) => |
83 def html_body(xml_body: XML.Body): XML.Body = |
84 html_class(Markup.Language.DOCUMENT, html_body(body)) |
84 xml_body map { |
85 case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(html_body(body)) |
85 case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) => |
86 case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(html_body(body)) |
86 html_class(Markup.Language.DOCUMENT, html_body(body)) |
87 case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => XML.no_text |
87 case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(html_body(body)) |
88 case XML.Elem(Markup.Markdown_List(kind), body) => |
88 case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(html_body(body)) |
89 if (kind == Markup.ENUMERATE) HTML.enum(html_body(body)) else HTML.list(html_body(body)) |
89 case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => XML.no_text |
90 case XML.Elem(markup, body) => |
90 case XML.Elem(Markup.Markdown_List(kind), body) => |
91 val name = markup.name |
91 if (kind == Markup.ENUMERATE) HTML.enum(html_body(body)) else HTML.list(html_body(body)) |
92 val html = |
92 case XML.Elem(markup, body) => |
93 markup.properties match { |
93 val name = markup.name |
94 case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD => |
94 val html = |
95 List(html_class(kind, html_body(body))) |
95 markup.properties match { |
96 case _ => |
96 case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD => |
97 html_body(body) |
97 List(html_class(kind, html_body(body))) |
|
98 case _ => |
|
99 html_body(body) |
|
100 } |
|
101 Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match { |
|
102 case Some(c) => html_class(c.toString, html) |
|
103 case None => html_class(name, html) |
98 } |
104 } |
99 Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match { |
105 case XML.Text(text) => |
100 case Some(c) => html_class(c.toString, html) |
106 XML.Text(Symbol.decode(text)) |
101 case None => html_class(name, html) |
107 } |
102 } |
108 |
103 case XML.Text(text) => |
109 html_body(xml) |
104 XML.Text(Symbol.decode(text)) |
110 } |
105 } |
|
106 |
111 |
107 |
112 |
108 /* PIDE HTML document */ |
113 /* PIDE HTML document */ |
109 |
114 |
110 def html_document( |
115 def html_document( |
497 html_context.init_fonts(file_path.dir) |
502 html_context.init_fonts(file_path.dir) |
498 |
503 |
499 val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short) |
504 val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short) |
500 HTML.write_document(file_path.dir, file_path.file_name, |
505 HTML.write_document(file_path.dir, file_path.file_name, |
501 List(HTML.title(file_title)), |
506 List(HTML.title(file_title)), |
502 List(html_context.head(file_title), html_context.source(html_body(xml)))) |
507 List(html_context.head(file_title), html_context.source(make_html_body(xml)))) |
503 |
508 |
504 List(HTML.link(file_name, HTML.text(file_title))) |
509 List(HTML.link(file_name, HTML.text(file_title))) |
505 } |
510 } |
506 |
511 |
507 val thy_title = "Theory " + thy_name.theory_base_name |
512 val thy_title = "Theory " + thy_name.theory_base_name |