uniform preview for Isabelle/jEdit and Isabelle/VSCode;
authorwenzelm
Fri Dec 22 17:19:53 2017 +0100 (18 months ago)
changeset 67260ecd607631bc7
parent 67259 e13e8816cf2a
child 67261 bce56b5a35d5
uniform preview for Isabelle/jEdit and Isabelle/VSCode;
src/Pure/Thy/present.scala
src/Tools/VSCode/extension/package.json
src/Tools/VSCode/src/preview_panel.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/Thy/present.scala	Fri Dec 22 16:26:14 2017 +0100
     1.2 +++ b/src/Pure/Thy/present.scala	Fri Dec 22 17:19:53 2017 +0100
     1.3 @@ -103,17 +103,23 @@
     1.4  
     1.5    /** preview **/
     1.6  
     1.7 -  def preview(fonts_dir: String, snapshot: Document.Snapshot, plain: Boolean = false): String =
     1.8 +  sealed case class Preview(title: String, content: String)
     1.9 +
    1.10 +  def preview(snapshot: Document.Snapshot,
    1.11 +    plain: Boolean = false,
    1.12 +    fonts_url: String => String = HTML.fonts_url()): Preview =
    1.13    {
    1.14      require(!snapshot.is_outdated)
    1.15  
    1.16      val name = snapshot.node_name
    1.17      if (name.is_bibtex && !plain) {
    1.18        val title = "Bibliography " + quote(name.path.base_name)
    1.19 -      Isabelle_System.with_tmp_file("bib", "bib") { bib =>
    1.20 -        File.write(bib, snapshot.node.source)
    1.21 -        Bibtex.html_output(List(bib), style = "unsort", title = title)
    1.22 -      }
    1.23 +      val content =
    1.24 +        Isabelle_System.with_tmp_file("bib", "bib") { bib =>
    1.25 +          File.write(bib, snapshot.node.source)
    1.26 +          Bibtex.html_output(List(bib), style = "unsort", title = title)
    1.27 +        }
    1.28 +      Preview(title, content)
    1.29      }
    1.30      else {
    1.31        val (title, body) =
    1.32 @@ -121,10 +127,12 @@
    1.33            ("Theory " + quote(name.theory_base_name), pide_document(snapshot))
    1.34          else ("File " + quote(name.path.base_name), text_document(snapshot))
    1.35  
    1.36 -      HTML.output_document(
    1.37 -        List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css)),
    1.38 -          HTML.title(title)),
    1.39 -          List(HTML.chapter(title), HTML.source(body)))
    1.40 +      val content =
    1.41 +        HTML.output_document(
    1.42 +          List(HTML.style(HTML.fonts_css(fonts_url) + File.read(HTML.isabelle_css)),
    1.43 +            HTML.title(title)), List(HTML.source(body)), css = "")
    1.44 +
    1.45 +      Preview(title, content)
    1.46      }
    1.47    }
    1.48  
     2.1 --- a/src/Tools/VSCode/extension/package.json	Fri Dec 22 16:26:14 2017 +0100
     2.2 +++ b/src/Tools/VSCode/extension/package.json	Fri Dec 22 17:19:53 2017 +0100
     2.3 @@ -25,6 +25,7 @@
     2.4      "activationEvents": [
     2.5          "onLanguage:isabelle",
     2.6          "onLanguage:isabelle-ml",
     2.7 +        "onLanguage:bibtex",
     2.8          "onCommand:isabelle.preview",
     2.9          "onCommand:isabelle.preview-split",
    2.10          "onCommand:isabelle.preview-source"
    2.11 @@ -107,11 +108,31 @@
    2.12                      "group": "navigation"
    2.13                  },
    2.14                  {
    2.15 +                    "when": "editorLangId == isabelle-ml",
    2.16 +                    "command": "isabelle.preview",
    2.17 +                    "group": "navigation"
    2.18 +                },
    2.19 +                {
    2.20 +                    "when": "editorLangId == bibtex",
    2.21 +                    "command": "isabelle.preview",
    2.22 +                    "group": "navigation"
    2.23 +                },
    2.24 +                {
    2.25                      "when": "editorLangId == isabelle",
    2.26                      "command": "isabelle.preview-split",
    2.27                      "group": "navigation"
    2.28                  },
    2.29                  {
    2.30 +                    "when": "editorLangId == isabelle-ml",
    2.31 +                    "command": "isabelle.preview-split",
    2.32 +                    "group": "navigation"
    2.33 +                },
    2.34 +                {
    2.35 +                    "when": "editorLangId == bibtex",
    2.36 +                    "command": "isabelle.preview-split",
    2.37 +                    "group": "navigation"
    2.38 +                },
    2.39 +                {
    2.40                      "when": "resourceScheme == isabelle-preview",
    2.41                      "command": "isabelle.preview-update",
    2.42                      "group": "navigation"
    2.43 @@ -127,6 +148,16 @@
    2.44                      "when": "resourceLangId == isabelle",
    2.45                      "command": "isabelle.preview",
    2.46                      "group": "navigation"
    2.47 +                },
    2.48 +                {
    2.49 +                    "when": "resourceLangId == isabelle-ml",
    2.50 +                    "command": "isabelle.preview",
    2.51 +                    "group": "navigation"
    2.52 +                },
    2.53 +                {
    2.54 +                    "when": "resourceLangId == bibtex",
    2.55 +                    "command": "isabelle.preview",
    2.56 +                    "group": "navigation"
    2.57                  }
    2.58              ]
    2.59          },
     3.1 --- a/src/Tools/VSCode/src/preview_panel.scala	Fri Dec 22 16:26:14 2017 +0100
     3.2 +++ b/src/Tools/VSCode/src/preview_panel.scala	Fri Dec 22 17:19:53 2017 +0100
     3.3 @@ -30,8 +30,9 @@
     3.4                val snapshot = model.snapshot()
     3.5                if (snapshot.is_outdated) m
     3.6                else {
     3.7 -                val (label, content) = make_preview(model, snapshot)
     3.8 -                channel.write(Protocol.Preview_Response(file, column, label, content))
     3.9 +                val preview = Present.preview(snapshot)
    3.10 +                channel.write(
    3.11 +                  Protocol.Preview_Response(file, column, preview.title, preview.content))
    3.12                  m - file
    3.13                }
    3.14              case None => m - file
    3.15 @@ -40,15 +41,4 @@
    3.16        (map1.nonEmpty, map1)
    3.17      })
    3.18    }
    3.19 -
    3.20 -  def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) =
    3.21 -  {
    3.22 -    val label = "Preview " + quote(model.node_name.theory_base_name)
    3.23 -    val content =
    3.24 -      HTML.output_document(
    3.25 -        List(HTML.style(HTML.fonts_css()), HTML.style_file(HTML.isabelle_css)),
    3.26 -        List(HTML.source(Present.pide_document(snapshot))),
    3.27 -        css = "")
    3.28 -    (label, content)
    3.29 -  }
    3.30  }
     4.1 --- a/src/Tools/jEdit/src/document_model.scala	Fri Dec 22 16:26:14 2017 +0100
     4.2 +++ b/src/Tools/jEdit/src/document_model.scala	Fri Dec 22 17:19:53 2017 +0100
     4.3 @@ -312,7 +312,8 @@
     4.4          }
     4.5          yield {
     4.6            val snapshot = model.await_stable_snapshot()
     4.7 -          HTTP.Response.html(Present.preview(fonts_root, snapshot))
     4.8 +          val preview = Present.preview(snapshot, fonts_url = HTML.fonts_dir(fonts_root))
     4.9 +          HTTP.Response.html(preview.content)
    4.10          })
    4.11  
    4.12      List(HTTP.fonts(fonts_root), preview)