equal
deleted
inserted
replaced
115 require(!snapshot.is_outdated) |
115 require(!snapshot.is_outdated) |
116 |
116 |
117 def output_document(title: String, body: XML.Body): String = |
117 def output_document(title: String, body: XML.Body): String = |
118 HTML.output_document( |
118 HTML.output_document( |
119 List( |
119 List( |
120 HTML.style(HTML.fonts_css(fonts_url) + File.read(HTML.isabelle_css)), |
120 HTML.style(HTML.fonts_css(fonts_url) + "\n\n" + File.read(HTML.isabelle_css)), |
121 HTML.title(title)), |
121 HTML.title(title)), |
122 List(HTML.source(body)), css = "", structural = false) |
122 List(HTML.source(body)), css = "", structural = false) |
123 |
123 |
124 val name = snapshot.node_name |
124 val name = snapshot.node_name |
125 |
125 |