--- a/NEWS Fri Dec 22 17:23:01 2017 +0100
+++ b/NEWS Fri Dec 22 17:49:51 2017 +0100
@@ -73,6 +73,9 @@
* Action "isabelle.preview" is able to present more file formats,
notably bibtex database files and plain text files.
+* Action "isabelle.draft" is similar to "isabelle.preview", but shows a
+plain-text document draft.
+
*** Isabelle/VSCode Prover IDE ***
--- a/src/Doc/JEdit/JEdit.thy Fri Dec 22 17:23:01 2017 +0100
+++ b/src/Doc/JEdit/JEdit.thy Fri Dec 22 17:49:51 2017 +0100
@@ -1902,6 +1902,9 @@
current document node in the default web browser. The content is derived
from the semantic markup produced by the prover, and thus depends on the
status of formal processing.
+
+ Action @{action_def isabelle.draft} is similar to @{action
+ isabelle.preview}, but shows a plain-text document draft.
\<close>
--- a/src/Pure/Thy/present.scala Fri Dec 22 17:23:01 2017 +0100
+++ b/src/Pure/Thy/present.scala Fri Dec 22 17:49:51 2017 +0100
@@ -106,13 +106,13 @@
sealed case class Preview(title: String, content: String)
def preview(snapshot: Document.Snapshot,
- plain: Boolean = false,
+ plain_text: Boolean = false,
fonts_url: String => String = HTML.fonts_url()): Preview =
{
require(!snapshot.is_outdated)
val name = snapshot.node_name
- if (name.is_bibtex && !plain) {
+ if (name.is_bibtex && !plain_text) {
val title = "Bibliography " + quote(name.path.base_name)
val content =
Isabelle_System.with_tmp_file("bib", "bib") { bib =>
@@ -123,7 +123,7 @@
}
else {
val (title, body) =
- if (name.is_theory && !plain)
+ if (name.is_theory && !plain_text)
("Theory " + quote(name.theory_base_name), pide_document(snapshot))
else ("File " + quote(name.path.base_name), text_document(snapshot))
--- a/src/Tools/jEdit/src/actions.xml Fri Dec 22 17:23:01 2017 +0100
+++ b/src/Tools/jEdit/src/actions.xml Fri Dec 22 17:49:51 2017 +0100
@@ -159,7 +159,12 @@
</ACTION>
<ACTION NAME="isabelle.preview">
<CODE>
- isabelle.jedit.Document_Model.open_preview(view);
+ isabelle.jedit.Document_Model.open_preview(view, false);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.draft">
+ <CODE>
+ isabelle.jedit.Document_Model.open_preview(view, true);
</CODE>
</ACTION>
<ACTION NAME="isabelle.keymap-merge">
--- a/src/Tools/jEdit/src/document_model.scala Fri Dec 22 17:23:01 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Fri Dec 22 17:49:51 2017 +0100
@@ -286,14 +286,16 @@
/* HTTP preview */
- def open_preview(view: View)
+ private val plain_text_prefix = "plain_text="
+
+ def open_preview(view: View, plain_text: Boolean)
{
Document_Model.get(view.getBuffer) match {
case Some(model) =>
val name = model.node_name
val url =
- PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root +
- "/preview?" + Url.encode(name.node)
+ PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview?" +
+ (if (plain_text) plain_text_prefix else "") + Url.encode(name.node)
PIDE.editor.hyperlink_url(url).follow(view)
case _ =>
}
@@ -307,12 +309,15 @@
val preview =
HTTP.get(preview_root, arg =>
for {
- query <- Library.try_unprefix(preview_root + "?", arg.uri.toString)
- model <- get(PIDE.resources.node_name(Url.decode(query)))
+ query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode(_))
+ name = Library.perhaps_unprefix(plain_text_prefix, query)
+ model <- get(PIDE.resources.node_name(name))
}
yield {
val snapshot = model.await_stable_snapshot()
- val preview = Present.preview(snapshot, fonts_url = HTML.fonts_dir(fonts_root))
+ val preview =
+ Present.preview(snapshot, fonts_url = HTML.fonts_dir(fonts_root),
+ plain_text = query.startsWith(plain_text_prefix))
HTTP.Response.html(preview.content)
})