# HG changeset patch
# User wenzelm
# Date 1513961391 -3600
# Node ID 46540a2ead4bc3185fff1048859166782e7e88a0
# Parent  bce56b5a35d5a64e0393eacf0956960e2c9f1001
action "isabelle.draft" for plain-text preview;

diff -r bce56b5a35d5 -r 46540a2ead4b NEWS
--- 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 ***
 
diff -r bce56b5a35d5 -r 46540a2ead4b src/Doc/JEdit/JEdit.thy
--- 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>
 
 
diff -r bce56b5a35d5 -r 46540a2ead4b src/Pure/Thy/present.scala
--- 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))
 
diff -r bce56b5a35d5 -r 46540a2ead4b src/Tools/jEdit/src/actions.xml
--- 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">
diff -r bce56b5a35d5 -r 46540a2ead4b src/Tools/jEdit/src/document_model.scala
--- 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)
         })