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;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
     1
/*  Title:      Tools/VSCode/src/preview.scala
65977
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
     3
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
     4
HTML document preview.
65977
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
     5
*/
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
     6
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
     7
package isabelle.vscode
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
     8
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
     9
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
    10
import isabelle._
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
    11
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
    12
import java.io.{File => JFile}
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
    13
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
    14
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    15
class Preview(resources: VSCode_Resources)
65977
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
    16
{
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    17
  private val pending = Synchronized(Map.empty[JFile, Int])
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    18
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    19
  def request(file: JFile, column: Int): Unit =
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    20
    pending.change(map => map + (file -> column))
65977
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
    21
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    22
  def flush(channel: Channel): Boolean =
65977
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
    23
  {
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    24
    pending.change_result(map =>
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    25
    {
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    26
      val map1 =
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    27
        (map /: map.iterator)({ case (m, (file, column)) =>
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    28
          resources.get_model(file) match {
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    29
            case Some(model) =>
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    30
              val snapshot = model.snapshot()
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    31
              if (snapshot.is_outdated) m
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    32
              else {
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    33
                val (label, content) = make_preview(model, snapshot)
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    34
                channel.write(Protocol.Preview_Response(file, column, label, content))
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    35
                m - file
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    36
              }
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    37
            case None => m - file
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    38
          }
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    39
        })
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    40
      (map1.nonEmpty, map1)
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    41
    })
65977
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
    42
  }
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
    43
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    44
  def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) =
65977
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
    45
  {
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    46
    val label = "Preview " + quote(model.node_name.toString)
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    47
    val content =
65996
e72f7291ad6c use css from Isabelle distribution;
wenzelm
parents: 65995
diff changeset
    48
      HTML.output_document(Nil,
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    49
        List(
65995
145283346958 clarified output;
wenzelm
parents: 65983
diff changeset
    50
          HTML.chapter("Theory " + quote(model.node_name.theory_base_name)),
65996
e72f7291ad6c use css from Isabelle distribution;
wenzelm
parents: 65995
diff changeset
    51
          HTML.source(Symbol.decode(snapshot.node.commands.iterator.map(_.source).mkString))),
e72f7291ad6c use css from Isabelle distribution;
wenzelm
parents: 65995
diff changeset
    52
        css = Url.print_file(Path.explode("~~/etc/isabelle.css").file))
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    53
    (label, content)
65977
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
    54
  }
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents:
diff changeset
    55
}