--- a/src/Pure/Thy/present.scala Fri Dec 22 16:26:14 2017 +0100
+++ b/src/Pure/Thy/present.scala Fri Dec 22 17:19:53 2017 +0100
@@ -103,17 +103,23 @@
/** preview **/
- def preview(fonts_dir: String, snapshot: Document.Snapshot, plain: Boolean = false): String =
+ sealed case class Preview(title: String, content: String)
+
+ def preview(snapshot: Document.Snapshot,
+ plain: Boolean = false,
+ fonts_url: String => String = HTML.fonts_url()): Preview =
{
require(!snapshot.is_outdated)
val name = snapshot.node_name
if (name.is_bibtex && !plain) {
val title = "Bibliography " + quote(name.path.base_name)
- Isabelle_System.with_tmp_file("bib", "bib") { bib =>
- File.write(bib, snapshot.node.source)
- Bibtex.html_output(List(bib), style = "unsort", title = title)
- }
+ val content =
+ Isabelle_System.with_tmp_file("bib", "bib") { bib =>
+ File.write(bib, snapshot.node.source)
+ Bibtex.html_output(List(bib), style = "unsort", title = title)
+ }
+ Preview(title, content)
}
else {
val (title, body) =
@@ -121,10 +127,12 @@
("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(title)),
- List(HTML.chapter(title), HTML.source(body)))
+ val content =
+ HTML.output_document(
+ List(HTML.style(HTML.fonts_css(fonts_url) + File.read(HTML.isabelle_css)),
+ HTML.title(title)), List(HTML.source(body)), css = "")
+
+ Preview(title, content)
}
}
--- a/src/Tools/VSCode/extension/package.json Fri Dec 22 16:26:14 2017 +0100
+++ b/src/Tools/VSCode/extension/package.json Fri Dec 22 17:19:53 2017 +0100
@@ -25,6 +25,7 @@
"activationEvents": [
"onLanguage:isabelle",
"onLanguage:isabelle-ml",
+ "onLanguage:bibtex",
"onCommand:isabelle.preview",
"onCommand:isabelle.preview-split",
"onCommand:isabelle.preview-source"
@@ -107,11 +108,31 @@
"group": "navigation"
},
{
+ "when": "editorLangId == isabelle-ml",
+ "command": "isabelle.preview",
+ "group": "navigation"
+ },
+ {
+ "when": "editorLangId == bibtex",
+ "command": "isabelle.preview",
+ "group": "navigation"
+ },
+ {
"when": "editorLangId == isabelle",
"command": "isabelle.preview-split",
"group": "navigation"
},
{
+ "when": "editorLangId == isabelle-ml",
+ "command": "isabelle.preview-split",
+ "group": "navigation"
+ },
+ {
+ "when": "editorLangId == bibtex",
+ "command": "isabelle.preview-split",
+ "group": "navigation"
+ },
+ {
"when": "resourceScheme == isabelle-preview",
"command": "isabelle.preview-update",
"group": "navigation"
@@ -127,6 +148,16 @@
"when": "resourceLangId == isabelle",
"command": "isabelle.preview",
"group": "navigation"
+ },
+ {
+ "when": "resourceLangId == isabelle-ml",
+ "command": "isabelle.preview",
+ "group": "navigation"
+ },
+ {
+ "when": "resourceLangId == bibtex",
+ "command": "isabelle.preview",
+ "group": "navigation"
}
]
},
--- a/src/Tools/VSCode/src/preview_panel.scala Fri Dec 22 16:26:14 2017 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala Fri Dec 22 17:19:53 2017 +0100
@@ -30,8 +30,9 @@
val snapshot = model.snapshot()
if (snapshot.is_outdated) m
else {
- val (label, content) = make_preview(model, snapshot)
- channel.write(Protocol.Preview_Response(file, column, label, content))
+ val preview = Present.preview(snapshot)
+ channel.write(
+ Protocol.Preview_Response(file, column, preview.title, preview.content))
m - file
}
case None => m - file
@@ -40,15 +41,4 @@
(map1.nonEmpty, map1)
})
}
-
- def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) =
- {
- val label = "Preview " + quote(model.node_name.theory_base_name)
- val content =
- HTML.output_document(
- List(HTML.style(HTML.fonts_css()), HTML.style_file(HTML.isabelle_css)),
- List(HTML.source(Present.pide_document(snapshot))),
- css = "")
- (label, content)
- }
}
--- a/src/Tools/jEdit/src/document_model.scala Fri Dec 22 16:26:14 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Fri Dec 22 17:19:53 2017 +0100
@@ -312,7 +312,8 @@
}
yield {
val snapshot = model.await_stable_snapshot()
- HTTP.Response.html(Present.preview(fonts_root, snapshot))
+ val preview = Present.preview(snapshot, fonts_url = HTML.fonts_dir(fonts_root))
+ HTTP.Response.html(preview.content)
})
List(HTTP.fonts(fonts_root), preview)