# HG changeset patch
# User wenzelm
# Date 1496699758 -7200
# Node ID 69b5ef78fb07b98f49d2fbf522ecfd7b3d487753
# Parent  9ce3720976dc5f84a801df0ca67262f1c2be08e3
HTML preview via builtin HTTP server;

diff -r 9ce3720976dc -r 69b5ef78fb07 NEWS
--- 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
diff -r 9ce3720976dc -r 69b5ef78fb07 src/Tools/jEdit/src/actions.xml
--- 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);
diff -r 9ce3720976dc -r 69b5ef78fb07 src/Tools/jEdit/src/document_model.scala
--- 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
diff -r 9ce3720976dc -r 69b5ef78fb07 src/Tools/jEdit/src/plugin.scala
--- 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 _)