103 |
103 |
104 /** preview **/ |
104 /** preview **/ |
105 |
105 |
106 sealed case class Preview(title: String, content: String) |
106 sealed case class Preview(title: String, content: String) |
107 |
107 |
108 def preview(snapshot: Document.Snapshot, |
108 def preview( |
|
109 resources: Resources, |
|
110 snapshot: Document.Snapshot, |
109 plain_text: Boolean = false, |
111 plain_text: Boolean = false, |
110 fonts_url: String => String = HTML.fonts_url()): Preview = |
112 fonts_url: String => String = HTML.fonts_url()): Preview = |
111 { |
113 { |
112 require(!snapshot.is_outdated) |
114 require(!snapshot.is_outdated) |
113 |
115 |
117 HTML.style(HTML.fonts_css(fonts_url) + File.read(HTML.isabelle_css)), |
119 HTML.style(HTML.fonts_css(fonts_url) + File.read(HTML.isabelle_css)), |
118 HTML.title(title)), |
120 HTML.title(title)), |
119 List(HTML.source(body)), css = "", structural = false) |
121 List(HTML.source(body)), css = "", structural = false) |
120 |
122 |
121 val name = snapshot.node_name |
123 val name = snapshot.node_name |
|
124 |
122 if (plain_text) { |
125 if (plain_text) { |
123 val title = "File " + quote(name.path.base_name) |
126 val title = "File " + quote(name.path.base_name) |
124 val content = output_document(title, HTML.text(snapshot.node.source)) |
127 val content = output_document(title, HTML.text(snapshot.node.source)) |
125 Preview(title, content) |
128 Preview(title, content) |
126 } |
129 } |
127 else if (name.is_bibtex) { |
|
128 val title = "Bibliography " + quote(name.path.base_name) |
|
129 val content = |
|
130 Isabelle_System.with_tmp_file("bib", "bib") { bib => |
|
131 File.write(bib, snapshot.node.source) |
|
132 Bibtex.html_output(List(bib), style = "unsort", title = title) |
|
133 } |
|
134 Preview(title, content) |
|
135 } |
|
136 else { |
130 else { |
137 val title = |
131 resources.make_preview(snapshot) match { |
138 if (name.is_theory) "Theory " + quote(name.theory_base_name) |
132 case Some(preview) => preview |
139 else "File " + quote(name.path.base_name) |
133 case None => |
140 val content = output_document(title, pide_document(snapshot)) |
134 val title = |
141 Preview(title, content) |
135 if (name.is_theory) "Theory " + quote(name.theory_base_name) |
|
136 else "File " + quote(name.path.base_name) |
|
137 val content = output_document(title, pide_document(snapshot)) |
|
138 Preview(title, content) |
|
139 } |
142 } |
140 } |
143 } |
141 } |
144 |
142 |
145 |
143 |
146 /* PIDE document */ |
144 /* PIDE document */ |