# HG changeset patch
# User wenzelm
# Date 1513892751 -3600
# Node ID b6282f149b50142ac40c893d347e177a636c181c
# Parent  a6d8458b48c0b713078d5e57c6f8edf579590c0d# Parent  68177abb29885015204701906f431334cb51d47b
merged

diff -r a6d8458b48c0 -r b6282f149b50 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Thu Dec 21 22:12:41 2017 +0100
+++ b/Admin/components/components.sha1	Thu Dec 21 22:45:51 2017 +0100
@@ -3,6 +3,7 @@
 81250148f8b89ac3587908fb20645081d7f53207  bash_process-1.2.1.tar.gz
 97b2491382130a841b3bbaebdcf8720c4d4fb227  bash_process-1.2.2.tar.gz
 9e21f447bfa0431ae5097301d553dd6df3c58218  bash_process-1.2.tar.gz
+a65ce644b6094d41e9f991ef851cf05eff5dd0a9  bib2xhtml-20171221.tar.gz
 e7ffe4238b61a3c1ee87aca4421e7a612e09b836  ci-extras-1.tar.gz
 70105fd6fbfd1a868383fc510772b95234325d31  csdp-6.x.tar.gz
 2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7  cvc3-2.4.1.tar.gz
diff -r a6d8458b48c0 -r b6282f149b50 Admin/components/main
--- a/Admin/components/main	Thu Dec 21 22:12:41 2017 +0100
+++ b/Admin/components/main	Thu Dec 21 22:45:51 2017 +0100
@@ -1,5 +1,6 @@
 #main components for everyday use, without big impact on overall build time
 bash_process-1.2.2
+bib2xhtml-20171221
 csdp-6.x
 cvc4-1.5-3
 e-2.0-1
diff -r a6d8458b48c0 -r b6282f149b50 NEWS
--- a/NEWS	Thu Dec 21 22:12:41 2017 +0100
+++ b/NEWS	Thu Dec 21 22:45:51 2017 +0100
@@ -70,6 +70,10 @@
 "isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
 arguments into this format.
 
+* Action "isabelle.preview" is able to present more file formats,
+notably bibtex database files and plain text files.
+
+
 
 *** Document preparation ***
 
diff -r a6d8458b48c0 -r b6282f149b50 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Thu Dec 21 22:12:41 2017 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Thu Dec 21 22:45:51 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 a6d8458b48c0 -r b6282f149b50 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Dec 21 22:12:41 2017 +0100
+++ b/src/Pure/General/http.scala	Thu Dec 21 22:45:51 2017 +0100
@@ -7,7 +7,7 @@
 package isabelle
 
 
-import java.net.{InetAddress, InetSocketAddress, URI, URLDecoder}
+import java.net.{InetAddress, InetSocketAddress, URI}
 import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
 
 import scala.collection.immutable.SortedMap
@@ -74,9 +74,7 @@
     def decode_properties: Properties.T =
       space_explode('&', request.text).map(s =>
         space_explode('=', s) match {
-          case List(a, b) =>
-            URLDecoder.decode(a, UTF8.charset_name) ->
-            URLDecoder.decode(b, UTF8.charset_name)
+          case List(a, b) => Url.decode(a) -> Url.decode(b)
           case _ => error("Malformed key-value pair in HTTP/POST: " + quote(s))
         })
   }
diff -r a6d8458b48c0 -r b6282f149b50 src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Thu Dec 21 22:12:41 2017 +0100
+++ b/src/Pure/General/url.scala	Thu Dec 21 22:45:51 2017 +0100
@@ -9,8 +9,7 @@
 
 import java.io.{File => JFile}
 import java.nio.file.{Paths, FileSystemNotFoundException}
-import java.net.{URI, URISyntaxException}
-import java.net.{URL, MalformedURLException}
+import java.net.{URI, URISyntaxException, URL, MalformedURLException, URLDecoder, URLEncoder}
 import java.util.zip.GZIPInputStream
 
 
@@ -34,6 +33,12 @@
     catch { case ERROR(_) => false }
 
 
+  /* strings */
+
+  def decode(s: String): String = URLDecoder.decode(s, UTF8.charset_name)
+  def encode(s: String): String = URLEncoder.encode(s, UTF8.charset_name)
+
+
   /* read */
 
   private def read(url: URL, gzip: Boolean): String =
diff -r a6d8458b48c0 -r b6282f149b50 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Dec 21 22:12:41 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Dec 21 22:45:51 2017 +0100
@@ -119,6 +119,8 @@
 
       def path: Path = Path.explode(File.standard_path(node))
 
+      def is_bibtex: Boolean = Bibtex.check_name(node)
+
       def is_theory: Boolean = theory.nonEmpty
 
       def theory_base_name: String = Long_Name.base_name(theory)
@@ -320,6 +322,12 @@
 
     def command_start(cmd: Command): Option[Text.Offset] =
       Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2)
+
+    def get_text: String =
+      get_blob match {
+        case Some(blob) => blob.bytes.text
+        case None => command_iterator(0).map({ case (cmd, _) => cmd.source }).mkString
+      }
   }
 
 
@@ -528,6 +536,7 @@
 
     def node_required: Boolean
     def get_blob: Option[Blob]
+    def is_bibtex: Boolean = node_name.is_bibtex
     def bibtex_entries: List[Text.Info[String]]
 
     def node_edits(
diff -r a6d8458b48c0 -r b6282f149b50 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Thu Dec 21 22:12:41 2017 +0100
+++ b/src/Pure/Thy/present.scala	Thu Dec 21 22:45:51 2017 +0100
@@ -128,9 +128,16 @@
     }
 
   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 =
+    snapshot.node.get_text match {
+      case "" => Nil
+      case txt => List(XML.Text(Symbol.decode(txt)))
+    }
 
 
 
diff -r a6d8458b48c0 -r b6282f149b50 src/Pure/Tools/bibtex.scala
--- a/src/Pure/Tools/bibtex.scala	Thu Dec 21 22:12:41 2017 +0100
+++ b/src/Pure/Tools/bibtex.scala	Thu Dec 21 22:45:51 2017 +0100
@@ -487,4 +487,88 @@
     }
     (chunks.toList, ctxt)
   }
+
+
+
+  /** HTML output **/
+
+  private val output_styles =
+    List(
+      "empty" -> "html-n",
+      "plain" -> "html-n",
+      "alpha" -> "html-a",
+      "named" -> "html-n",
+      "paragraph" -> "html-n",
+      "unsort" -> "html-u",
+      "unsortlist" -> "html-u")
+
+  def html_output(bib: List[Path],
+    body: Boolean = false,
+    citations: List[String] = List("*"),
+    style: String = "empty",
+    chronological: Boolean = false): String =
+  {
+    Isabelle_System.with_tmp_dir("bibtex")(tmp_dir =>
+    {
+      /* database files */
+
+      val bib_files = bib.map(path => path.split_ext._1)
+      val bib_names =
+      {
+        val names0 = bib_files.map(_.base_name)
+        if (Library.duplicates(names0).isEmpty) names0
+        else names0.zipWithIndex.map({ case (name, i) => (i + 1).toString + "-" + name })
+      }
+
+      for ((a, b) <- bib_files zip bib_names) {
+        File.copy(a.ext("bib"), tmp_dir + Path.basic(b).ext("bib"))
+      }
+
+
+      /* style file */
+
+      val bst =
+        output_styles.toMap.get(style) match {
+          case Some(base) => base + (if (chronological) "c" else "") + ".bst"
+          case None =>
+            error("Bad style for bibtex HTML output: " + quote(style) +
+              "\n(expected: " + commas_quote(output_styles.map(_._1)) + ")")
+        }
+      File.copy(Path.explode("$BIB2XHTML_HOME/bst") + Path.explode(bst), tmp_dir)
+
+
+      /* result */
+
+      val in_file = Path.explode("bib.aux")
+      val out_file = Path.explode("bib.html")
+
+      File.write(tmp_dir + in_file,
+        bib_names.mkString("\\bibdata{", ",", "}\n") +
+        citations.map(cite => "\\citation{" + cite + "}\n").mkString)
+
+      Isabelle_System.bash(
+        "\"$BIB2XHTML_HOME/main/bib2xhtml.pl\" -B \"$ISABELLE_BIBTEX\"" +
+          " -u -s " + Bash.string(style) + (if (chronological) " -c " else " ") +
+          File.bash_path(in_file) + " " + File.bash_path(out_file),
+        cwd = tmp_dir.file).check
+
+      val html = File.read(tmp_dir + out_file)
+
+      if (body) {
+        cat_lines(
+          split_lines(html).
+            dropWhile(line => !line.startsWith("<!-- BEGIN BIBLIOGRAPHY")).reverse.
+            dropWhile(line => !line.startsWith("<!-- END BIBLIOGRAPHY")).reverse)
+      }
+      else html
+    })
+  }
+
+  def present(snapshot: Document.Snapshot): String =
+  {
+    Isabelle_System.with_tmp_file("bib", "bib") { bib =>
+      File.write(bib, snapshot.node.get_text)
+      html_output(List(bib), style = "unsortlist")
+    }
+  }
 }
diff -r a6d8458b48c0 -r b6282f149b50 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Dec 21 22:12:41 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Dec 21 22:45:51 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)
   }
 }
 
@@ -324,12 +329,19 @@
   {
     val snapshot = await_stable_snapshot()
 
-    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 = "")
+    if (is_bibtex) Bibtex.present(snapshot)
+    else {
+      HTML.output_document(
+        List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_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))))
+    }
   }
 
 
@@ -428,7 +440,7 @@
     else Some(Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty))
 
   def bibtex_entries: List[Text.Info[String]] =
-    if (Bibtex.check_name(node_name)) content.bibtex_entries else Nil
+    if (is_bibtex) content.bibtex_entries else Nil
 
 
   /* edits */
@@ -549,7 +561,7 @@
 
   def bibtex_entries: List[Text.Info[String]] =
     GUI_Thread.require {
-      if (Bibtex.check_name(node_name)) {
+      if (node_name.is_bibtex) {
         _bibtex_entries match {
           case Some(entries) => entries
           case None =>