--- a/src/Pure/Thy/present.scala Fri Dec 22 13:51:20 2017 +0100
+++ b/src/Pure/Thy/present.scala Fri Dec 22 14:27:59 2017 +0100
@@ -101,6 +101,28 @@
}
+ /** preview **/
+
+ def preview(fonts_dir: String, snapshot: Document.Snapshot, plain: Boolean = false): String =
+ {
+ require(!snapshot.is_outdated)
+
+ val name = snapshot.node_name
+ if (name.is_bibtex && !plain) Bibtex.present(snapshot)
+ else {
+ val (heading, body) =
+ if (name.is_theory && !plain)
+ ("Theory " + quote(name.theory_base_name), pide_document(snapshot))
+ else ("File " + quote(name.path.base_name), text_document(snapshot))
+
+ HTML.output_document(
+ List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css)),
+ HTML.title(heading)),
+ List(HTML.chapter(heading), HTML.source(body)))
+ }
+ }
+
+
/* theory document */
private val document_span_elements =
@@ -127,7 +149,7 @@
XML.Text(Symbol.decode(text))
}
- def theory_document(snapshot: Document.Snapshot): XML.Body =
+ def pide_document(snapshot: Document.Snapshot): XML.Body =
make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements))
--- a/src/Tools/VSCode/src/preview_panel.scala Fri Dec 22 13:51:20 2017 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala Fri Dec 22 14:27:59 2017 +0100
@@ -47,7 +47,7 @@
val content =
HTML.output_document(
List(HTML.style(HTML.fonts_css()), HTML.style_file(HTML.isabelle_css)),
- List(HTML.source(Present.theory_document(snapshot))),
+ List(HTML.source(Present.pide_document(snapshot))),
css = "")
(label, content)
}
--- a/src/Tools/jEdit/src/document_model.scala Fri Dec 22 13:51:20 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Fri Dec 22 14:27:59 2017 +0100
@@ -313,7 +313,10 @@
{ case (name, model)
if url_name == (if (name.is_theory) name.theory else name.node) => model })
}
- yield HTTP.Response.html(model.preview(fonts_root)))
+ yield {
+ val snapshot = model.await_stable_snapshot()
+ HTTP.Response.html(Present.preview(fonts_root, snapshot))
+ })
List(HTTP.fonts(fonts_root), preview)
}
@@ -321,29 +324,6 @@
sealed abstract class Document_Model extends Document.Model
{
- /* content */
-
- def bibtex_entries: List[Text.Info[String]]
-
- def preview(fonts_dir: String): String =
- {
- val snapshot = await_stable_snapshot()
-
- if (is_bibtex) Bibtex.present(snapshot)
- else {
- val (heading, body) =
- if (is_theory)
- ("Theory " + quote(node_name.theory_base_name), Present.theory_document(snapshot))
- else ("File " + quote(node_name.path.base_name), Present.text_document(snapshot))
-
- HTML.output_document(
- List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css)),
- HTML.title(heading)),
- List(HTML.chapter(heading), HTML.source(body)))
- }
- }
-
-
/* perspective */
def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil