HTML preview via builtin HTTP server;
authorwenzelm
Mon Jun 05 23:55:58 2017 +0200 (23 months ago)
changeset 6601969b5ef78fb07
parent 66018 9ce3720976dc
child 66020 a31760eee09d
HTML preview via builtin HTTP server;
NEWS
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/NEWS	Mon Jun 05 23:13:08 2017 +0200
     1.2 +++ b/NEWS	Mon Jun 05 23:55:58 2017 +0200
     1.3 @@ -52,6 +52,9 @@
     1.4  
     1.5  *** Prover IDE -- Isabelle/Scala/jEdit ***
     1.6  
     1.7 +* Action "isabelle.preview" opens an HTML preview of the current theory
     1.8 +document in the default web browser.
     1.9 +
    1.10  * Command-line invocation "isabelle jedit -R -l SESSION" uses the parent
    1.11  image of the SESSION, with qualified theory imports restricted to that
    1.12  portion of the session graph. Moreover, the ROOT entry of the SESSION is
     2.1 --- a/src/Tools/jEdit/src/actions.xml	Mon Jun 05 23:13:08 2017 +0200
     2.2 +++ b/src/Tools/jEdit/src/actions.xml	Mon Jun 05 23:55:58 2017 +0200
     2.3 @@ -152,6 +152,11 @@
     2.4  	    isabelle.jedit.Isabelle.plugin_options(view);
     2.5  	  </CODE>
     2.6  	</ACTION>
     2.7 +	<ACTION NAME="isabelle.preview">
     2.8 +	  <CODE>
     2.9 +	    isabelle.jedit.Document_Model.open_preview(view);
    2.10 +	  </CODE>
    2.11 +	</ACTION>
    2.12  	<ACTION NAME="isabelle.keymap-merge">
    2.13  	  <CODE>
    2.14  	    isabelle.jedit.Keymap_Merge.check_dialog(view);
     3.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Jun 05 23:13:08 2017 +0200
     3.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Jun 05 23:55:58 2017 +0200
     3.3 @@ -14,6 +14,7 @@
     3.4  import java.io.{File => JFile}
     3.5  
     3.6  import scala.collection.mutable
     3.7 +import scala.annotation.tailrec
     3.8  
     3.9  import org.gjt.sp.jedit.{jEdit, View}
    3.10  import org.gjt.sp.jedit.Buffer
    3.11 @@ -264,6 +265,36 @@
    3.12        try { Bibtex.document_entries(text) }
    3.13        catch { case ERROR(msg) => Output.warning(msg); Nil }
    3.14    }
    3.15 +
    3.16 +
    3.17 +  /* HTTP preview */
    3.18 +
    3.19 +  def open_preview(view: View)
    3.20 +  {
    3.21 +    Document_Model.get(view.getBuffer) match {
    3.22 +      case Some(model) =>
    3.23 +        JEdit_Editor.hyperlink_url(
    3.24 +          PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview/" +
    3.25 +            model.node_name.theory).follow(view)
    3.26 +      case None =>
    3.27 +    }
    3.28 +  }
    3.29 +
    3.30 +  def http_handlers(http_root: String): List[HTTP.Handler] =
    3.31 +  {
    3.32 +    val preview_root = http_root + "/preview"
    3.33 +    val preview =
    3.34 +      HTTP.get(preview_root, uri =>
    3.35 +        for {
    3.36 +          theory <- Library.try_unprefix(preview_root + "/", uri.toString)
    3.37 +          model <-
    3.38 +            get_models().iterator.collectFirst(
    3.39 +              { case (node_name, model) if node_name.theory == theory => model })
    3.40 +        }
    3.41 +        yield HTTP.Response.html(model.preview("../fonts")))
    3.42 +
    3.43 +    List(HTTP.fonts(http_root + "/fonts"), preview)
    3.44 +  }
    3.45  }
    3.46  
    3.47  sealed abstract class Document_Model extends Document.Model
    3.48 @@ -272,6 +303,18 @@
    3.49  
    3.50    def bibtex_entries: List[Text.Info[String]]
    3.51  
    3.52 +  def preview(fonts_dir: String): String =
    3.53 +  {
    3.54 +    val snapshot = await_stable_snapshot()
    3.55 +
    3.56 +    HTML.output_document(
    3.57 +      List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css))),
    3.58 +      List(
    3.59 +        HTML.chapter("Theory " + quote(node_name.theory_base_name)),
    3.60 +        HTML.source(snapshot.node.commands.iterator.map(_.source).mkString)),
    3.61 +      css = "")
    3.62 +  }
    3.63 +
    3.64  
    3.65    /* perspective */
    3.66  
    3.67 @@ -299,6 +342,19 @@
    3.68      }
    3.69      else (false, Document.Node.no_perspective_text)
    3.70    }
    3.71 +
    3.72 +
    3.73 +  /* snapshot */
    3.74 +
    3.75 +  @tailrec final def await_stable_snapshot(): Document.Snapshot =
    3.76 +  {
    3.77 +    val snapshot = this.snapshot()
    3.78 +    if (snapshot.is_outdated) {
    3.79 +      Thread.sleep(PIDE.options.seconds("editor_output_delay").ms)
    3.80 +      await_stable_snapshot()
    3.81 +    }
    3.82 +    else snapshot
    3.83 +  }
    3.84  }
    3.85  
    3.86  object File_Model
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Jun 05 23:13:08 2017 +0200
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Jun 05 23:55:58 2017 +0200
     4.3 @@ -12,6 +12,7 @@
     4.4  import javax.swing.JOptionPane
     4.5  
     4.6  import java.io.{File => JFile}
     4.7 +import java.util.UUID
     4.8  
     4.9  import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
    4.10  import org.gjt.sp.jedit.textarea.JEditTextArea
    4.11 @@ -393,6 +394,13 @@
    4.12    }
    4.13  
    4.14  
    4.15 +  /* HTTP server */
    4.16 +
    4.17 +  val http_root: String = "/" + UUID.randomUUID().toString
    4.18 +
    4.19 +  val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))
    4.20 +
    4.21 +
    4.22    /* start and stop */
    4.23  
    4.24    override def start()
    4.25 @@ -418,6 +426,8 @@
    4.26        init_mode_provider()
    4.27        JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
    4.28  
    4.29 +      http_server.start
    4.30 +
    4.31        startup_failure = None
    4.32      }
    4.33      catch {
    4.34 @@ -430,6 +440,8 @@
    4.35  
    4.36    override def stop()
    4.37    {
    4.38 +    http_server.stop
    4.39 +
    4.40      exit_mode_provider()
    4.41      JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
    4.42