# HG changeset patch
# User wenzelm
# Date 1513959593 -3600
# Node ID ecd607631bc7eee0bc43eec5e68d0a5b182409a9
# Parent  e13e8816cf2a07ccbd9b57b418c1b3b60b605008
uniform preview for Isabelle/jEdit and Isabelle/VSCode;

diff -r e13e8816cf2a -r ecd607631bc7 src/Pure/Thy/present.scala
--- 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)
     }
   }
 
diff -r e13e8816cf2a -r ecd607631bc7 src/Tools/VSCode/extension/package.json
--- 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"
                 }
             ]
         },
diff -r e13e8816cf2a -r ecd607631bc7 src/Tools/VSCode/src/preview_panel.scala
--- 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)
-  }
 }
diff -r e13e8816cf2a -r ecd607631bc7 src/Tools/jEdit/src/document_model.scala
--- 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)