src/Tools/VSCode/src/preview.scala
author wenzelm
Thu, 01 Jun 2017 21:14:38 +0200
changeset 65996 e72f7291ad6c
parent 65995 145283346958
child 65998 d07300e8a14d
permissions -rw-r--r--
use css from Isabelle distribution;

/*  Title:      Tools/VSCode/src/preview.scala
    Author:     Makarius

HTML document preview.
*/

package isabelle.vscode


import isabelle._

import java.io.{File => JFile}


class Preview(resources: VSCode_Resources)
{
  private val pending = Synchronized(Map.empty[JFile, Int])

  def request(file: JFile, column: Int): Unit =
    pending.change(map => map + (file -> column))

  def flush(channel: Channel): Boolean =
  {
    pending.change_result(map =>
    {
      val map1 =
        (map /: map.iterator)({ case (m, (file, column)) =>
          resources.get_model(file) match {
            case Some(model) =>
              val snapshot = model.snapshot()
              if (snapshot.is_outdated) m
              else {
                val (label, content) = make_preview(model, snapshot)
                channel.write(Protocol.Preview_Response(file, column, label, content))
                m - file
              }
            case None => m - file
          }
        })
      (map1.nonEmpty, map1)
    })
  }

  def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) =
  {
    val label = "Preview " + quote(model.node_name.toString)
    val content =
      HTML.output_document(Nil,
        List(
          HTML.chapter("Theory " + quote(model.node_name.theory_base_name)),
          HTML.source(Symbol.decode(snapshot.node.commands.iterator.map(_.source).mkString))),
        css = Url.print_file(Path.explode("~~/etc/isabelle.css").file))
    (label, content)
  }
}