# HG changeset patch
# User wenzelm
# Date 1513890450 -3600
# Node ID 4cedf44f2af168266646d436d5dca21ef0898213
# Parent  caa4c900100991790c901d943ac98afbb36d7a3a
isabelle.preview presents auxiliary text files as well;

diff -r caa4c9001009 -r 4cedf44f2af1 NEWS
--- a/NEWS	Thu Dec 21 21:44:09 2017 +0100
+++ b/NEWS	Thu Dec 21 22:07:30 2017 +0100
@@ -70,6 +70,9 @@
 "isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
 arguments into this format.
 
+* Action "isabelle.preview" presents auxiliary text files as well.
+
+
 
 *** Document preparation ***
 
diff -r caa4c9001009 -r 4cedf44f2af1 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Thu Dec 21 21:44:09 2017 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Thu Dec 21 22:07:30 2017 +0100
@@ -1899,7 +1899,7 @@
 
 text \<open>
   The action @{action_def isabelle.preview} opens an HTML preview of the
-  current theory document in the default web browser. The content is derived
+  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.
 \<close>
diff -r caa4c9001009 -r 4cedf44f2af1 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Thu Dec 21 21:44:09 2017 +0100
+++ b/src/Pure/Thy/present.scala	Thu Dec 21 22:07:30 2017 +0100
@@ -128,8 +128,19 @@
     }
 
   def theory_document(snapshot: Document.Snapshot): XML.Body =
+    make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements))
+
+
+  /* text document */
+
+  def text_document(snapshot: Document.Snapshot): XML.Body =
   {
-    make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements))
+    val text =
+      snapshot.node.get_blob match {
+        case Some(blob) => blob.bytes.text
+        case None => ""
+      }
+    if (text.isEmpty) Nil else List(XML.Text(Symbol.decode(text)))
   }
 
 
diff -r caa4c9001009 -r 4cedf44f2af1 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Dec 21 21:44:09 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Dec 21 22:07:30 2017 +0100
@@ -289,28 +289,33 @@
   def open_preview(view: View)
   {
     Document_Model.get(view.getBuffer) match {
-      case Some(model) if model.is_theory =>
-        PIDE.editor.hyperlink_url(
-          PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview/" +
-            model.node_name.theory).follow(view)
+      case Some(model) =>
+        val name = model.node_name
+        val url =
+          PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview?" +
+            Url.encode(if (name.is_theory) name.theory else name.node)
+        PIDE.editor.hyperlink_url(url).follow(view)
       case _ =>
     }
   }
 
   def http_handlers(http_root: String): List[HTTP.Handler] =
   {
+    val fonts_root = http_root + "/fonts"
     val preview_root = http_root + "/preview"
+
     val preview =
       HTTP.get(preview_root, arg =>
         for {
-          theory <- Library.try_unprefix(preview_root + "/", arg.uri.toString)
+          url_name <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode(_))
           model <-
             get_models().iterator.collectFirst(
-              { case (node_name, model) if node_name.theory == theory => model })
+              { case (name, model)
+                if url_name == (if (name.is_theory) name.theory else name.node) => model })
         }
-        yield HTTP.Response.html(model.preview("../fonts")))
+        yield HTTP.Response.html(model.preview(fonts_root)))
 
-    List(HTTP.fonts(http_root + "/fonts"), preview)
+    List(HTTP.fonts(fonts_root), preview)
   }
 }
 
@@ -326,10 +331,14 @@
 
     HTML.output_document(
       List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css))),
-      List(
-        HTML.chapter("Theory " + quote(node_name.theory_base_name)),
-        HTML.source(Present.theory_document(snapshot))),
-      css = "")
+        css = "",
+        body =
+          if (is_theory)
+            List(HTML.chapter("Theory " + quote(node_name.theory_base_name)),
+              HTML.source(Present.theory_document(snapshot)))
+          else
+            List(HTML.chapter("File " + quote(node_name.node)),
+              HTML.source(Present.text_document(snapshot))))
   }