--- 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
--- 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
--- 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 ***
--- 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>
--- 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))
})
}
--- 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 =
--- 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(
--- 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)))
+ }
--- 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")
+ }
+ }
}
--- 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 =>