--- a/NEWS Mon Jun 05 23:13:08 2017 +0200
+++ b/NEWS Mon Jun 05 23:55:58 2017 +0200
@@ -52,6 +52,9 @@
*** Prover IDE -- Isabelle/Scala/jEdit ***
+* Action "isabelle.preview" opens an HTML preview of the current theory
+document in the default web browser.
+
* Command-line invocation "isabelle jedit -R -l SESSION" uses the parent
image of the SESSION, with qualified theory imports restricted to that
portion of the session graph. Moreover, the ROOT entry of the SESSION is
--- a/src/Tools/jEdit/src/actions.xml Mon Jun 05 23:13:08 2017 +0200
+++ b/src/Tools/jEdit/src/actions.xml Mon Jun 05 23:55:58 2017 +0200
@@ -152,6 +152,11 @@
isabelle.jedit.Isabelle.plugin_options(view);
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.preview">
+ <CODE>
+ isabelle.jedit.Document_Model.open_preview(view);
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.keymap-merge">
<CODE>
isabelle.jedit.Keymap_Merge.check_dialog(view);
--- a/src/Tools/jEdit/src/document_model.scala Mon Jun 05 23:13:08 2017 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Mon Jun 05 23:55:58 2017 +0200
@@ -14,6 +14,7 @@
import java.io.{File => JFile}
import scala.collection.mutable
+import scala.annotation.tailrec
import org.gjt.sp.jedit.{jEdit, View}
import org.gjt.sp.jedit.Buffer
@@ -264,6 +265,36 @@
try { Bibtex.document_entries(text) }
catch { case ERROR(msg) => Output.warning(msg); Nil }
}
+
+
+ /* HTTP preview */
+
+ def open_preview(view: View)
+ {
+ Document_Model.get(view.getBuffer) match {
+ case Some(model) =>
+ JEdit_Editor.hyperlink_url(
+ PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview/" +
+ model.node_name.theory).follow(view)
+ case None =>
+ }
+ }
+
+ def http_handlers(http_root: String): List[HTTP.Handler] =
+ {
+ val preview_root = http_root + "/preview"
+ val preview =
+ HTTP.get(preview_root, uri =>
+ for {
+ theory <- Library.try_unprefix(preview_root + "/", uri.toString)
+ model <-
+ get_models().iterator.collectFirst(
+ { case (node_name, model) if node_name.theory == theory => model })
+ }
+ yield HTTP.Response.html(model.preview("../fonts")))
+
+ List(HTTP.fonts(http_root + "/fonts"), preview)
+ }
}
sealed abstract class Document_Model extends Document.Model
@@ -272,6 +303,18 @@
def bibtex_entries: List[Text.Info[String]]
+ def preview(fonts_dir: String): String =
+ {
+ 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(snapshot.node.commands.iterator.map(_.source).mkString)),
+ css = "")
+ }
+
/* perspective */
@@ -299,6 +342,19 @@
}
else (false, Document.Node.no_perspective_text)
}
+
+
+ /* snapshot */
+
+ @tailrec final def await_stable_snapshot(): Document.Snapshot =
+ {
+ val snapshot = this.snapshot()
+ if (snapshot.is_outdated) {
+ Thread.sleep(PIDE.options.seconds("editor_output_delay").ms)
+ await_stable_snapshot()
+ }
+ else snapshot
+ }
}
object File_Model
--- a/src/Tools/jEdit/src/plugin.scala Mon Jun 05 23:13:08 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Mon Jun 05 23:55:58 2017 +0200
@@ -12,6 +12,7 @@
import javax.swing.JOptionPane
import java.io.{File => JFile}
+import java.util.UUID
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
import org.gjt.sp.jedit.textarea.JEditTextArea
@@ -393,6 +394,13 @@
}
+ /* HTTP server */
+
+ val http_root: String = "/" + UUID.randomUUID().toString
+
+ val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))
+
+
/* start and stop */
override def start()
@@ -418,6 +426,8 @@
init_mode_provider()
JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
+ http_server.start
+
startup_failure = None
}
catch {
@@ -430,6 +440,8 @@
override def stop()
{
+ http_server.stop
+
exit_mode_provider()
JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)