src/Tools/jEdit/src/document_model.scala
changeset 66019 69b5ef78fb07
parent 65469 78ace4a14975
child 66036 b6396880b644
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Jun 05 23:13:08 2017 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Jun 05 23:55:58 2017 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4  import java.io.{File => JFile}
     1.5  
     1.6  import scala.collection.mutable
     1.7 +import scala.annotation.tailrec
     1.8  
     1.9  import org.gjt.sp.jedit.{jEdit, View}
    1.10  import org.gjt.sp.jedit.Buffer
    1.11 @@ -264,6 +265,36 @@
    1.12        try { Bibtex.document_entries(text) }
    1.13        catch { case ERROR(msg) => Output.warning(msg); Nil }
    1.14    }
    1.15 +
    1.16 +
    1.17 +  /* HTTP preview */
    1.18 +
    1.19 +  def open_preview(view: View)
    1.20 +  {
    1.21 +    Document_Model.get(view.getBuffer) match {
    1.22 +      case Some(model) =>
    1.23 +        JEdit_Editor.hyperlink_url(
    1.24 +          PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview/" +
    1.25 +            model.node_name.theory).follow(view)
    1.26 +      case None =>
    1.27 +    }
    1.28 +  }
    1.29 +
    1.30 +  def http_handlers(http_root: String): List[HTTP.Handler] =
    1.31 +  {
    1.32 +    val preview_root = http_root + "/preview"
    1.33 +    val preview =
    1.34 +      HTTP.get(preview_root, uri =>
    1.35 +        for {
    1.36 +          theory <- Library.try_unprefix(preview_root + "/", uri.toString)
    1.37 +          model <-
    1.38 +            get_models().iterator.collectFirst(
    1.39 +              { case (node_name, model) if node_name.theory == theory => model })
    1.40 +        }
    1.41 +        yield HTTP.Response.html(model.preview("../fonts")))
    1.42 +
    1.43 +    List(HTTP.fonts(http_root + "/fonts"), preview)
    1.44 +  }
    1.45  }
    1.46  
    1.47  sealed abstract class Document_Model extends Document.Model
    1.48 @@ -272,6 +303,18 @@
    1.49  
    1.50    def bibtex_entries: List[Text.Info[String]]
    1.51  
    1.52 +  def preview(fonts_dir: String): String =
    1.53 +  {
    1.54 +    val snapshot = await_stable_snapshot()
    1.55 +
    1.56 +    HTML.output_document(
    1.57 +      List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css))),
    1.58 +      List(
    1.59 +        HTML.chapter("Theory " + quote(node_name.theory_base_name)),
    1.60 +        HTML.source(snapshot.node.commands.iterator.map(_.source).mkString)),
    1.61 +      css = "")
    1.62 +  }
    1.63 +
    1.64  
    1.65    /* perspective */
    1.66  
    1.67 @@ -299,6 +342,19 @@
    1.68      }
    1.69      else (false, Document.Node.no_perspective_text)
    1.70    }
    1.71 +
    1.72 +
    1.73 +  /* snapshot */
    1.74 +
    1.75 +  @tailrec final def await_stable_snapshot(): Document.Snapshot =
    1.76 +  {
    1.77 +    val snapshot = this.snapshot()
    1.78 +    if (snapshot.is_outdated) {
    1.79 +      Thread.sleep(PIDE.options.seconds("editor_output_delay").ms)
    1.80 +      await_stable_snapshot()
    1.81 +    }
    1.82 +    else snapshot
    1.83 +  }
    1.84  }
    1.85  
    1.86  object File_Model