src/Pure/Thy/presentation.scala
author wenzelm
Mon, 04 Jan 2021 13:23:51 +0100
changeset 73042 22f5a6283477
parent 73041 66b45c3389d3
child 73043 759b6869377d
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Thy/present.scala
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
     3
72957
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
     4
HTML/PDF presentation of theory documents.
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
     5
*/
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
     6
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
     7
package isabelle
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
     8
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
     9
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    10
import scala.collection.immutable.SortedMap
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    11
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    12
72652
07edf1952ab1 clarified modules;
wenzelm
parents: 72650
diff changeset
    13
object Presentation
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
    14
{
72957
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    15
  /** HTML documents **/
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    16
72962
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    17
  val fonts_path = Path.explode("fonts")
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    18
72957
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    19
  sealed case class HTML_Document(title: String, content: String)
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    20
72959
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
    21
  def html_context(fonts_url: String => String = HTML.fonts_url()): HTML_Context =
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
    22
    new HTML_Context(fonts_url)
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
    23
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
    24
  final class HTML_Context private[Presentation](fonts_url: String => String)
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
    25
  {
72962
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    26
    def init_fonts(dir: Path)
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    27
    {
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    28
      val fonts_dir = Isabelle_System.make_directory(dir + fonts_path)
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    29
      for (entry <- Isabelle_Fonts.fonts(hidden = true))
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    30
        File.copy(entry.path, fonts_dir)
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    31
    }
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    32
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    33
    def head(title: String, rest: XML.Body = Nil): XML.Tree =
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    34
      HTML.div("head", HTML.chapter(title) :: rest)
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    35
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    36
    def source(body: XML.Body): XML.Tree = HTML.pre("source", body)
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    37
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    38
    def contents(heading: String, items: List[XML.Body], css_class: String = "contents")
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    39
      : List[XML.Elem] =
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    40
    {
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    41
      if (items.isEmpty) Nil
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    42
      else List(HTML.div(css_class, List(HTML.section(heading), HTML.itemize(items))))
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    43
    }
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
    44
72959
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
    45
    def output_document(title: String, body: XML.Body): String =
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
    46
      HTML.output_document(
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
    47
        List(
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
    48
          HTML.style(HTML.fonts_css(fonts_url) + "\n\n" + File.read(HTML.isabelle_css)),
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
    49
          HTML.title(title)),
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
    50
        List(HTML.source(body)), css = "", structural = false)
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
    51
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
    52
    def html_document(title: String, body: XML.Body): HTML_Document =
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
    53
      HTML_Document(title, output_document(title, body))
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
    54
  }
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
    55
72957
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    56
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    57
  /* HTML body */
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    58
73036
b028e8d22d8d clarified HTML presentation elements;
wenzelm
parents: 73028
diff changeset
    59
  val html_elements1: Markup.Elements =
b028e8d22d8d clarified HTML presentation elements;
wenzelm
parents: 73028
diff changeset
    60
    Rendering.foreground_elements ++ Rendering.text_color_elements +
b028e8d22d8d clarified HTML presentation elements;
wenzelm
parents: 73028
diff changeset
    61
      Markup.NUMERAL + Markup.COMMENT
b028e8d22d8d clarified HTML presentation elements;
wenzelm
parents: 73028
diff changeset
    62
b028e8d22d8d clarified HTML presentation elements;
wenzelm
parents: 73028
diff changeset
    63
  val html_elements2: Markup.Elements =
b028e8d22d8d clarified HTML presentation elements;
wenzelm
parents: 73028
diff changeset
    64
    html_elements1 ++ Rendering.markdown_elements + Markup.LANGUAGE
b028e8d22d8d clarified HTML presentation elements;
wenzelm
parents: 73028
diff changeset
    65
72957
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    66
  private val div_elements =
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    67
    Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    68
      HTML.descr.name)
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    69
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    70
  private def html_div(html: XML.Body): Boolean =
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    71
    html exists {
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    72
      case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body)
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    73
      case XML.Text(_) => false
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    74
    }
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    75
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    76
  private def html_class(c: String, html: XML.Body): XML.Tree =
73028
95e0f014cd24 tuned signature;
wenzelm
parents: 73022
diff changeset
    77
    if (html.forall(_ == XML.no_text)) XML.no_text
72957
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    78
    else if (html_div(html)) HTML.div(c, html)
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    79
    else HTML.span(c, html)
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    80
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    81
  private def html_body(xml: XML.Body): XML.Body =
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    82
    xml map {
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    83
      case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) =>
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    84
        html_class(Markup.Language.DOCUMENT, html_body(body))
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    85
      case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(html_body(body))
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    86
      case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(html_body(body))
73028
95e0f014cd24 tuned signature;
wenzelm
parents: 73022
diff changeset
    87
      case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => XML.no_text
72957
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    88
      case XML.Elem(Markup.Markdown_List(kind), body) =>
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    89
        if (kind == Markup.ENUMERATE) HTML.enum(html_body(body)) else HTML.list(html_body(body))
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    90
      case XML.Elem(markup, body) =>
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    91
        val name = markup.name
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    92
        val html =
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    93
          markup.properties match {
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    94
            case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    95
              List(html_class(kind, html_body(body)))
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    96
            case _ =>
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    97
              html_body(body)
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    98
          }
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
    99
        Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   100
          case Some(c) => html_class(c.toString, html)
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   101
          case None => html_class(name, html)
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   102
        }
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   103
      case XML.Text(text) =>
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   104
        XML.Text(Symbol.decode(text))
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   105
    }
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   106
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   107
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   108
  /* PIDE HTML document */
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   109
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   110
  def html_document(
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   111
    resources: Resources,
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   112
    snapshot: Document.Snapshot,
72962
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
   113
    html_context: HTML_Context,
73036
b028e8d22d8d clarified HTML presentation elements;
wenzelm
parents: 73028
diff changeset
   114
    html_elements: Markup.Elements,
72959
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
   115
    plain_text: Boolean = false): HTML_Document =
72957
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   116
  {
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   117
    require(!snapshot.is_outdated)
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   118
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   119
    val name = snapshot.node_name
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   120
    if (plain_text) {
72962
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
   121
      val title = "File " + Symbol.cartouche_decoded(name.path.file_name)
72959
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
   122
      val body = HTML.text(snapshot.node.source)
72962
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
   123
      html_context.html_document(title, body)
72957
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   124
    }
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   125
    else {
72962
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
   126
      resources.html_document(snapshot) getOrElse {
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
   127
        val title =
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
   128
          if (name.is_theory) "Theory " + quote(name.theory_base_name)
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
   129
          else "File " + Symbol.cartouche_decoded(name.path.file_name)
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
   130
        val body = html_body(snapshot.xml_markup(elements = html_elements))
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
   131
        html_context.html_document(title, body)
72957
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   132
      }
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   133
    }
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   134
  }
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   135
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   136
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   137
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   138
  /** PDF LaTeX documents **/
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   139
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   140
  /* document info */
72649
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   141
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   142
  abstract class Document_Name
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   143
  {
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   144
    def name: String
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   145
    def path: Path = Path.basic(name)
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   146
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   147
    override def toString: String = name
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   148
  }
72683
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   149
72649
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   150
  object Document_Variant
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   151
  {
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   152
    def parse(name: String, tags: String): Document_Variant =
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   153
      Document_Variant(name, Library.space_explode(',', tags))
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   154
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   155
    def parse(opt: String): Document_Variant =
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   156
      Library.space_explode('=', opt) match {
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   157
        case List(name) => Document_Variant(name, Nil)
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   158
        case List(name, tags) => parse(name, tags)
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   159
        case _ => error("Malformed document variant: " + quote(opt))
72649
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   160
      }
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   161
  }
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   162
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   163
  sealed case class Document_Variant(name: String, tags: List[String]) extends Document_Name
72649
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   164
  {
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   165
    def print_tags: String = tags.mkString(",")
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   166
    def print: String = if (tags.isEmpty) name else name + "=" + print_tags
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   167
72649
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   168
    def latex_sty: String =
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   169
      Library.terminate_lines(
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   170
        tags.map(tag =>
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   171
          tag.toList match {
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   172
            case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}"
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   173
            case '-' :: cs => "\\isadroptag{" + cs.mkString + "}"
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   174
            case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   175
            case cs => "\\isakeeptag{" + cs.mkString + "}"
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   176
          }))
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   177
  }
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   178
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   179
  sealed case class Document_Input(name: String, sources: SHA1.Digest)
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   180
    extends Document_Name
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   181
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   182
  sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes)
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   183
    extends Document_Name
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   184
  {
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   185
    def log: String = log_xz.uncompress().text
72699
ed59a506998f clarified document_output vs. progress;
wenzelm
parents: 72696
diff changeset
   186
    def log_lines: List[String] = split_lines(log)
72700
c6981f55e60d tuned signature;
wenzelm
parents: 72699
diff changeset
   187
72880
wenzelm
parents: 72854
diff changeset
   188
    def write(db: SQL.Database, session_name: String): Unit =
72700
c6981f55e60d tuned signature;
wenzelm
parents: 72699
diff changeset
   189
      write_document(db, session_name, this)
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   190
  }
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   191
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   192
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   193
  /* SQL data model */
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   194
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   195
  object Data
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   196
  {
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   197
    val session_name = SQL.Column.string("session_name").make_primary_key
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   198
    val name = SQL.Column.string("name").make_primary_key
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   199
    val sources = SQL.Column.string("sources")
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   200
    val log_xz = SQL.Column.bytes("log_xz")
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   201
    val pdf = SQL.Column.bytes("pdf")
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   202
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   203
    val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf))
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   204
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   205
    def where_equal(session_name: String, name: String = ""): SQL.Source =
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   206
      "WHERE " + Data.session_name.equal(session_name) +
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   207
        (if (name == "") "" else " AND " + Data.name.equal(name))
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   208
  }
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   209
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   210
  def read_documents(db: SQL.Database, session_name: String): List[Document_Input] =
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   211
  {
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   212
    val select = Data.table.select(List(Data.name, Data.sources), Data.where_equal(session_name))
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   213
    db.using_statement(select)(stmt =>
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   214
      stmt.execute_query().iterator(res =>
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   215
      {
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   216
        val name = res.string(Data.name)
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   217
        val sources = res.string(Data.sources)
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   218
        Document_Input(name, SHA1.fake(sources))
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   219
      }).toList)
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   220
  }
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   221
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   222
  def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_Output] =
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   223
  {
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   224
    val select = Data.table.select(sql = Data.where_equal(session_name, name))
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   225
    db.using_statement(select)(stmt =>
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   226
    {
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   227
      val res = stmt.execute_query()
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   228
      if (res.next()) {
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   229
        val name = res.string(Data.name)
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   230
        val sources = res.string(Data.sources)
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   231
        val log_xz = res.bytes(Data.log_xz)
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   232
        val pdf = res.bytes(Data.pdf)
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   233
        Some(Document_Output(name, SHA1.fake(sources), log_xz, pdf))
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   234
      }
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   235
      else None
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   236
    })
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   237
  }
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   238
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   239
  def write_document(db: SQL.Database, session_name: String, doc: Document_Output)
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   240
  {
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   241
    db.using_statement(Data.table.insert())(stmt =>
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   242
    {
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   243
      stmt.string(1) = session_name
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   244
      stmt.string(2) = doc.name
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   245
      stmt.string(3) = doc.sources.toString
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   246
      stmt.bytes(4) = doc.log_xz
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   247
      stmt.bytes(5) = doc.pdf
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   248
      stmt.execute()
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   249
    })
72649
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   250
  }
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   251
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   252
72648
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   253
  /* presentation context */
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   254
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   255
  object Context
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   256
  {
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   257
    val none: Context = new Context { def enabled: Boolean = false }
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   258
    val standard: Context = new Context { def enabled: Boolean = true }
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   259
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   260
    def dir(path: Path): Context =
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   261
      new Context {
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   262
        def enabled: Boolean = true
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   263
        override def dir(store: Sessions.Store): Path = path
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   264
      }
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   265
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   266
    def make(s: String): Context =
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   267
      if (s == ":") standard else dir(Path.explode(s))
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   268
  }
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   269
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   270
  abstract class Context private
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   271
  {
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   272
    def enabled: Boolean
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   273
    def enabled(info: Sessions.Info): Boolean = enabled || info.browser_info
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   274
    def dir(store: Sessions.Store): Path = store.presentation_dir
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   275
    def dir(store: Sessions.Store, info: Sessions.Info): Path =
72670
4db9411c859c tuned signature;
wenzelm
parents: 72669
diff changeset
   276
      dir(store) + Path.explode(info.chapter_session)
72648
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   277
  }
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   278
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   279
72957
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   280
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   281
  /** HTML presentation **/
75fc90edc0a8 clarified signature and module structure;
wenzelm
parents: 72956
diff changeset
   282
72955
942bf91545fa clarified comments: file-system access is always unsynchronized;
wenzelm
parents: 72882
diff changeset
   283
  /* maintain chapter index */
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
   284
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   285
  private val sessions_path = Path.basic(".sessions")
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
   286
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
   287
  private def read_sessions(dir: Path): List[(String, String)] =
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
   288
  {
51416
e2505a192a7c do not absorb I/O errors;
wenzelm
parents: 51406
diff changeset
   289
    val path = dir + sessions_path
e2505a192a7c do not absorb I/O errors;
wenzelm
parents: 51406
diff changeset
   290
    if (path.is_file) {
e2505a192a7c do not absorb I/O errors;
wenzelm
parents: 51406
diff changeset
   291
      import XML.Decode._
65344
b99283eed13c clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents: 65089
diff changeset
   292
      list(pair(string, string))(Symbol.decode_yxml(File.read(path)))
51416
e2505a192a7c do not absorb I/O errors;
wenzelm
parents: 51406
diff changeset
   293
    }
e2505a192a7c do not absorb I/O errors;
wenzelm
parents: 51406
diff changeset
   294
    else Nil
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
   295
  }
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
   296
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
   297
  private def write_sessions(dir: Path, sessions: List[(String, String)])
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
   298
  {
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
   299
    import XML.Encode._
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
   300
    File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions)))
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
   301
  }
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
   302
61372
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   303
  def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)])
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   304
  {
72376
04bce3478688 clarified signature;
wenzelm
parents: 72375
diff changeset
   305
    val dir = Isabelle_System.make_directory(browser_info + Path.basic(chapter))
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
   306
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   307
    val sessions0 =
51406
950b897f95bb proper path -- I/O was hidden due to permissiveness;
wenzelm
parents: 51402
diff changeset
   308
      try { read_sessions(dir) }
51987
7d8e0e3c553b tuned signature;
wenzelm
parents: 51416
diff changeset
   309
      catch { case _: XML.Error => Nil }
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   310
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
   311
    val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
65988
8040d2563593 modernized generated HTML;
wenzelm
parents: 65404
diff changeset
   312
    write_sessions(dir, sessions)
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
   313
65988
8040d2563593 modernized generated HTML;
wenzelm
parents: 65404
diff changeset
   314
    val title = "Isabelle/" + chapter + " sessions"
8040d2563593 modernized generated HTML;
wenzelm
parents: 65404
diff changeset
   315
    HTML.write_document(dir, "index.html",
8040d2563593 modernized generated HTML;
wenzelm
parents: 65404
diff changeset
   316
      List(HTML.title(title + " (" + Distribution.version + ")")),
8040d2563593 modernized generated HTML;
wenzelm
parents: 65404
diff changeset
   317
      HTML.chapter(title) ::
8040d2563593 modernized generated HTML;
wenzelm
parents: 65404
diff changeset
   318
       (if (sessions.isEmpty) Nil
8040d2563593 modernized generated HTML;
wenzelm
parents: 65404
diff changeset
   319
        else
65992
50daca61efd6 tuned signature;
wenzelm
parents: 65989
diff changeset
   320
          List(HTML.div("sessions",
50daca61efd6 tuned signature;
wenzelm
parents: 65989
diff changeset
   321
            List(HTML.description(
65988
8040d2563593 modernized generated HTML;
wenzelm
parents: 65404
diff changeset
   322
              sessions.map({ case (name, description) =>
69318
f3351bb4390e clarified presentation;
wenzelm
parents: 69255
diff changeset
   323
                val descr = Symbol.trim_blank_lines(description)
65989
68cd15585f46 tuned layout;
wenzelm
parents: 65988
diff changeset
   324
                (List(HTML.link(name + "/index.html", HTML.text(name))),
69318
f3351bb4390e clarified presentation;
wenzelm
parents: 69255
diff changeset
   325
                  if (descr == "") Nil
f3351bb4390e clarified presentation;
wenzelm
parents: 69255
diff changeset
   326
                  else HTML.break ::: List(HTML.pre(HTML.text(descr)))) })))))))
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
   327
  }
61372
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   328
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   329
  def make_global_index(browser_info: Path)
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   330
  {
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   331
    if (!(browser_info + Path.explode("index.html")).is_file) {
72375
e48d93811ed7 clarified signature;
wenzelm
parents: 72309
diff changeset
   332
      Isabelle_System.make_directory(browser_info)
61372
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   333
      File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   334
        browser_info + Path.explode("isabelle.gif"))
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   335
      File.write(browser_info + Path.explode("index.html"),
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   336
        File.read(Path.explode("~~/lib/html/library_index_header.template")) +
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   337
        File.read(Path.explode("~~/lib/html/library_index_content.template")) +
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   338
        File.read(Path.explode("~~/lib/html/library_index_footer.template")))
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   339
    }
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   340
  }
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   341
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   342
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   343
  /* present session */
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   344
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   345
  val session_graph_path = Path.explode("session_graph.pdf")
72959
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
   346
  val readme_path = Path.explode("README.html")
a093b8fc9e21 tuned signature: more explicit types;
wenzelm
parents: 72957
diff changeset
   347
  val files_path = Path.explode("files")
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   348
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   349
  def html_name(name: Document.Node.Name): String = name.theory_base_name + ".html"
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   350
73042
22f5a6283477 tuned signature;
wenzelm
parents: 73041
diff changeset
   351
  def theory_link(deps: Sessions.Deps, session0: String,
22f5a6283477 tuned signature;
wenzelm
parents: 73041
diff changeset
   352
    name: Document.Node.Name, body: XML.Body): XML.Tree =
22f5a6283477 tuned signature;
wenzelm
parents: 73041
diff changeset
   353
  {
22f5a6283477 tuned signature;
wenzelm
parents: 73041
diff changeset
   354
    val session1 = deps(session0).theory_qualifier(name)
22f5a6283477 tuned signature;
wenzelm
parents: 73041
diff changeset
   355
    val info0 = deps.sessions_structure(session0)
22f5a6283477 tuned signature;
wenzelm
parents: 73041
diff changeset
   356
    val info1 = deps.sessions_structure(session1)
22f5a6283477 tuned signature;
wenzelm
parents: 73041
diff changeset
   357
    HTML.link(info0.relative_path(info1) + html_name(name), body)
22f5a6283477 tuned signature;
wenzelm
parents: 73041
diff changeset
   358
  }
22f5a6283477 tuned signature;
wenzelm
parents: 73041
diff changeset
   359
72669
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   360
  def token_markups(keywords: Keyword.Keywords, tok: Token): List[String] = {
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   361
    if (keywords.is_command(tok, Keyword.theory_end))
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   362
      List(Markup.KEYWORD2, Markup.KEYWORD)
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   363
    else if (keywords.is_command(tok, Keyword.proof_asm))
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   364
      List(Markup.KEYWORD3, Markup.COMMAND)
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   365
    else if (keywords.is_command(tok, Keyword.improper))
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   366
      List(Markup.KEYWORD1, Markup.IMPROPER, Markup.COMMAND)
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   367
    else if (tok.is_command) List(Markup.KEYWORD1, Markup.COMMAND)
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   368
    else if (tok.is_delimiter) List(Markup.DELIMITER, Markup.KEYWORD)
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   369
    else if (tok.is_keyword) List(Markup.KEYWORD2, Markup.KEYWORD)
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   370
    else if (tok.is_comment) List(Markup.COMMENT)
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   371
    else {
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   372
      tok.kind match {
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   373
        case Token.Kind.VAR => List(Markup.VAR)
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   374
        case Token.Kind.TYPE_IDENT => List(Markup.TFREE)
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   375
        case Token.Kind.TYPE_VAR => List(Markup.TVAR)
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   376
        case Token.Kind.STRING => List(Markup.STRING)
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   377
        case Token.Kind.ALT_STRING => List(Markup.ALT_STRING)
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   378
        case Token.Kind.VERBATIM => List(Markup.VERBATIM)
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   379
        case Token.Kind.CARTOUCHE => List(Markup.CARTOUCHE)
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   380
        case _ => Nil
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   381
      }
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   382
    }
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   383
  }
61372
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   384
72648
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   385
  def session_html(
72962
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
   386
    resources: Resources,
72648
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   387
    session: String,
1cbac4ae934d more explicit presentation directory;
wenzelm
parents: 72634
diff changeset
   388
    deps: Sessions.Deps,
72683
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   389
    db_context: Sessions.Database_Context,
72992
bcba32fd89de more interrupts;
wenzelm
parents: 72989
diff changeset
   390
    progress: Progress = new Progress,
73022
38528017e4c8 more verbosity for potentially bulky presentation;
wenzelm
parents: 72992
diff changeset
   391
    verbose: Boolean = false,
72962
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
   392
    html_context: HTML_Context,
73036
b028e8d22d8d clarified HTML presentation elements;
wenzelm
parents: 73028
diff changeset
   393
    html_elements: Markup.Elements,
72683
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   394
    presentation: Context)
61372
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   395
  {
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   396
    val info = deps.sessions_structure(session)
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   397
    val options = info.options
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   398
    val base = deps(session)
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   399
72683
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   400
    val session_dir = presentation.dir(db_context.store, info)
72962
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
   401
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
   402
    html_context.init_fonts(session_dir)
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   403
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   404
    Bytes.write(session_dir + session_graph_path,
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   405
      graphview.Graph_File.make_pdf(options, base.session_graph_display))
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   406
72673
8ff7a0e394f9 clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents: 72670
diff changeset
   407
    val documents =
72683
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   408
      for {
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   409
        doc <- info.document_variants
72716
7cef6b1a6682 clarified signature;
wenzelm
parents: 72700
diff changeset
   410
        document <- db_context.input_database(session)(read_document(_, _, doc.name))
73022
38528017e4c8 more verbosity for potentially bulky presentation;
wenzelm
parents: 72992
diff changeset
   411
      } yield {
38528017e4c8 more verbosity for potentially bulky presentation;
wenzelm
parents: 72992
diff changeset
   412
        if (verbose) progress.echo("Presenting document " + session + "/" + doc.name)
38528017e4c8 more verbosity for potentially bulky presentation;
wenzelm
parents: 72992
diff changeset
   413
        Bytes.write(session_dir + doc.path.pdf, document.pdf)
38528017e4c8 more verbosity for potentially bulky presentation;
wenzelm
parents: 72992
diff changeset
   414
        doc
38528017e4c8 more verbosity for potentially bulky presentation;
wenzelm
parents: 72992
diff changeset
   415
      }
72673
8ff7a0e394f9 clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents: 72670
diff changeset
   416
73041
wenzelm
parents: 73036
diff changeset
   417
    val view_links =
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   418
    {
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   419
      val deps_link =
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   420
        HTML.link(session_graph_path, HTML.text("theory dependencies"))
61372
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   421
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   422
      val readme_links =
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   423
        if ((info.dir + readme_path).is_file) {
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   424
          File.copy(info.dir + readme_path, session_dir + readme_path)
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   425
          List(HTML.link(readme_path, HTML.text("README")))
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   426
        }
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   427
        else Nil
62971
087e36ce0593 back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents: 62631
diff changeset
   428
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   429
      val document_links =
72673
8ff7a0e394f9 clarified PDF/HTML presentation, based on pdf blobs from session database (e.g. from earlier builds);
wenzelm
parents: 72670
diff changeset
   430
        documents.map(doc => HTML.link(doc.path.pdf, HTML.text(doc.name)))
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   431
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   432
      Library.separate(HTML.break ::: HTML.nl,
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   433
        (deps_link :: readme_links ::: document_links).
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   434
          map(link => HTML.text("View ") ::: List(link))).flatten
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   435
    }
62971
087e36ce0593 back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents: 62631
diff changeset
   436
72989
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   437
    val theories: List[XML.Body] =
72962
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
   438
    {
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
   439
      var seen_files = List.empty[(Path, String, Document.Node.Name)]
af2d0e07493b present auxiliary files with PIDE markup;
wenzelm
parents: 72959
diff changeset
   440
72989
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   441
      for (thy_name <- base.session_theories)
72669
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   442
      yield {
72992
bcba32fd89de more interrupts;
wenzelm
parents: 72989
diff changeset
   443
        progress.expose_interrupt()
73022
38528017e4c8 more verbosity for potentially bulky presentation;
wenzelm
parents: 72992
diff changeset
   444
        if (verbose) progress.echo("Presenting theory " + thy_name)
72992
bcba32fd89de more interrupts;
wenzelm
parents: 72989
diff changeset
   445
72989
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   446
        val syntax = base.theory_syntax(thy_name)
72669
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   447
        val keywords = syntax.keywords
72989
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   448
        val spans = syntax.parse_spans(Symbol.decode(File.read(thy_name.path)))
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   449
72669
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   450
        val thy_body =
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   451
        {
72989
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   452
          val imports_offset = base.known_theories(thy_name.theory).header.imports_offset
72669
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   453
          var token_offset = 1
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   454
          spans.flatMap(span =>
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   455
          {
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   456
            val is_init = span.is_kind(keywords, Keyword.theory_begin, false)
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   457
            span.content.flatMap(tok =>
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   458
            {
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   459
              val text = HTML.text(tok.source)
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   460
              val item =
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   461
                if (is_init && imports_offset.isDefinedAt(token_offset)) {
73042
22f5a6283477 tuned signature;
wenzelm
parents: 73041
diff changeset
   462
                  List(theory_link(deps, session, imports_offset(token_offset), text))
72669
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   463
                }
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   464
                else text
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   465
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   466
              token_offset += tok.symbol_length
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   467
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   468
              (token_markups(keywords, tok) :\ item)(
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   469
                { case (c, body) => List(HTML.span(c, body)) })
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   470
            })
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   471
          })
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   472
        }
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   473
72989
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   474
        val files =
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   475
          (for {
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   476
            thy_command <-
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   477
              Build_Job.read_theory(db_context, resources, session, thy_name.theory).iterator
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   478
            snapshot = Document.State.init.snippet(thy_command)
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   479
            (src_path, xml) <- snapshot.xml_markup_blobs(elements = html_elements).iterator
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   480
            if xml.nonEmpty
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   481
          } yield {
72992
bcba32fd89de more interrupts;
wenzelm
parents: 72989
diff changeset
   482
            progress.expose_interrupt()
bcba32fd89de more interrupts;
wenzelm
parents: 72989
diff changeset
   483
72989
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   484
            val file_name = (files_path + src_path.squash.html).implode
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   485
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   486
            seen_files.find(p => p._1 == src_path || p._2 == file_name) match {
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   487
              case None => seen_files ::= (src_path, file_name, thy_name)
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   488
              case Some((_, _, thy_name1)) =>
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   489
                error("Incoherent use of file name " + src_path + " as " + quote(file_name) +
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   490
                  " in theory " + thy_name1 + " vs. " + thy_name)
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   491
            }
72669
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   492
73022
38528017e4c8 more verbosity for potentially bulky presentation;
wenzelm
parents: 72992
diff changeset
   493
            if (verbose) progress.echo("Presenting file " + src_path)
38528017e4c8 more verbosity for potentially bulky presentation;
wenzelm
parents: 72992
diff changeset
   494
72989
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   495
            val file_path = session_dir + Path.explode(file_name)
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   496
            html_context.init_fonts(file_path.dir)
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   497
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   498
            val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short)
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   499
            HTML.write_document(file_path.dir, file_path.file_name,
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   500
              List(HTML.title(file_title)),
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   501
              List(html_context.head(file_title), html_context.source(html_body(xml))))
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   502
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   503
            List(HTML.link(file_name, HTML.text(file_title)))
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   504
          }).toList
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   505
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   506
        val thy_title = "Theory " + thy_name.theory_base_name
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   507
        HTML.write_document(session_dir, html_name(thy_name),
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   508
          List(HTML.title(thy_title)),
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   509
          List(html_context.head(thy_title), html_context.source(thy_body)))
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   510
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   511
        List(HTML.link(html_name(thy_name),
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   512
          HTML.text(thy_name.theory_base_name) :::
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   513
            (if (files.isEmpty) Nil else List(HTML.itemize(files)))))
72669
5e7916535860 generate theory HTML in Isabelle/Scala;
wenzelm
parents: 72665
diff changeset
   514
      }
72989
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   515
    }
61500
56a167b31a7f Isabelle fonts via external component;
wenzelm
parents: 61484
diff changeset
   516
72622
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   517
    val title = "Session " + session
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   518
    HTML.write_document(session_dir, "index.html",
830222403681 HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents: 72600
diff changeset
   519
      List(HTML.title(title + " (" + Distribution.version + ")")),
73041
wenzelm
parents: 73036
diff changeset
   520
      html_context.head(title, List(HTML.par(view_links))) ::
72989
5906162c8dd4 clarified presentation of files for each theory;
wenzelm
parents: 72963
diff changeset
   521
        html_context.contents("Theories", theories))
61372
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   522
  }
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   523
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   524
72682
e0443773ef1a clarified modules;
wenzelm
parents: 72675
diff changeset
   525
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   526
  /** build documents **/
72565
wenzelm
parents: 72376
diff changeset
   527
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   528
  val session_tex_path = Path.explode("session.tex")
72565
wenzelm
parents: 72376
diff changeset
   529
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   530
  def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex"
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   531
  def document_tex_name(name: Document.Node.Name): String = "document/" + tex_name(name)
72309
564012e31db1 discontinued obsolete DVI document format and related settings/tools;
wenzelm
parents: 71114
diff changeset
   532
72882
1dc2ad97e062 more informative error;
wenzelm
parents: 72880
diff changeset
   533
  class Build_Error(val log_lines: List[String], val message: String)
1dc2ad97e062 more informative error;
wenzelm
parents: 72880
diff changeset
   534
    extends Exn.User_Error(message)
1dc2ad97e062 more informative error;
wenzelm
parents: 72880
diff changeset
   535
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   536
  def build_documents(
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   537
    session: String,
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   538
    deps: Sessions.Deps,
72683
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   539
    db_context: Sessions.Database_Context,
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   540
    progress: Progress = new Progress,
72675
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   541
    output_sources: Option[Path] = None,
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   542
    output_pdf: Option[Path] = None,
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   543
    verbose: Boolean = false,
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   544
    verbose_latex: Boolean = false): List[Document_Output] =
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   545
  {
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   546
    /* session info */
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   547
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   548
    val info = deps.sessions_structure(session)
72854
6c660f05f70c clarified signature;
wenzelm
parents: 72847
diff changeset
   549
    val hierarchy = deps.sessions_structure.hierarchy(session)
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   550
    val options = info.options
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   551
    val base = deps(session)
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   552
    val graph_pdf = graphview.Graph_File.make_pdf(options, base.session_graph_display)
67177
af5b89bc065c removed obsolete option (see 74a1b722507e);
wenzelm
parents: 67176
diff changeset
   553
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   554
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   555
    /* prepare document directory */
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   556
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72599
diff changeset
   557
    lazy val tex_files =
72683
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   558
      for (name <- base.session_theories ::: base.document_theories)
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   559
      yield {
72854
6c660f05f70c clarified signature;
wenzelm
parents: 72847
diff changeset
   560
        val entry = db_context.get_export(hierarchy, name.theory, document_tex_name(name))
72847
9dda93a753b1 clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents: 72763
diff changeset
   561
        Path.basic(tex_name(name)) -> entry.uncompressed
72683
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   562
      }
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72599
diff changeset
   563
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   564
    def prepare_dir1(dir: Path, doc: Document_Variant): (Path, String) =
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   565
    {
72649
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   566
      val doc_dir = dir + Path.basic(doc.name)
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   567
      Isabelle_System.make_directory(doc_dir)
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   568
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   569
      Isabelle_System.bash("isabelle latex -o sty", cwd = doc_dir.file).check
72649
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   570
      File.write(doc_dir + Path.explode("isabelletags.sty"), doc.latex_sty)
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   571
      for ((base_dir, src) <- info.document_files) File.copy_base(info.dir + base_dir, src, doc_dir)
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   572
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   573
      File.write(doc_dir + session_tex_path,
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   574
        Library.terminate_lines(
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   575
          base.session_theories.map(name => "\\input{" + tex_name(name) + "}")))
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   576
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 72599
diff changeset
   577
      for ((path, tex) <- tex_files) Bytes.write(doc_dir + path, tex)
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   578
72649
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   579
      val root1 = "root_" + doc.name
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   580
      val root = if ((doc_dir + Path.explode(root1).tex).is_file) root1 else "root"
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   581
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   582
      (doc_dir, root)
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   583
    }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   584
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   585
    def prepare_dir2(dir: Path, doc: Document_Variant): Unit =
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   586
    {
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   587
      val doc_dir = dir + Path.basic(doc.name)
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   588
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   589
      // non-deterministic, but irrelevant
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   590
      Bytes.write(doc_dir + session_graph_path, graph_pdf)
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   591
    }
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   592
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   593
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   594
    /* produce documents */
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   595
72649
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   596
    val documents =
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   597
      for (doc <- info.documents)
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   598
      yield {
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   599
        Isabelle_System.with_tmp_dir("document")(tmp_dir =>
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   600
        {
72699
ed59a506998f clarified document_output vs. progress;
wenzelm
parents: 72696
diff changeset
   601
          progress.echo("Preparing " + session + "/" + doc.name + " ...")
72665
7e5102e11c5e clarified messages;
wenzelm
parents: 72663
diff changeset
   602
          val start = Time.now()
7e5102e11c5e clarified messages;
wenzelm
parents: 72663
diff changeset
   603
7e5102e11c5e clarified messages;
wenzelm
parents: 72663
diff changeset
   604
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   605
          // prepare sources
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   606
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   607
          val (doc_dir, root) = prepare_dir1(tmp_dir, doc)
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   608
          val digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   609
          val sources = SHA1.digest_set(digests)
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   610
          prepare_dir2(tmp_dir, doc)
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   611
72675
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   612
          for (dir <- output_sources) {
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   613
            prepare_dir1(dir, doc)
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   614
            prepare_dir2(dir, doc)
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   615
          }
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   616
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   617
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   618
          // old document from database
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   619
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   620
          val old_document =
72683
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   621
            for {
72716
7cef6b1a6682 clarified signature;
wenzelm
parents: 72700
diff changeset
   622
              old_doc <- db_context.input_database(session)(read_document(_, _, doc.name))
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   623
              if old_doc.sources == sources
72683
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   624
            }
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   625
            yield {
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   626
              Bytes.write(doc_dir + doc.path.pdf, old_doc.pdf)
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   627
              old_doc
72683
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   628
            }
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   629
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   630
          old_document getOrElse {
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   631
            // bash scripts
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   632
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   633
            def root_bash(ext: String): String = Bash.string(root + "." + ext)
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   634
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   635
            def latex_bash(fmt: String = "pdf", ext: String = "tex"): String =
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   636
              "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root + "." + ext)
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   637
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   638
            def bash(items: String*): Process_Result =
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   639
              progress.bash(items.mkString(" && "), cwd = doc_dir.file,
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   640
                echo = verbose_latex, watchdog = Time.seconds(0.5))
67204
849a838f7e57 purge log files -- avoid old errors;
wenzelm
parents: 67203
diff changeset
   641
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   642
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   643
            // prepare document
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   644
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   645
            val result =
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   646
              if ((doc_dir + Path.explode("build")).is_file) {
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   647
                bash("./build pdf " + Bash.string(doc.name))
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   648
              }
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   649
              else {
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   650
                bash(
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   651
                  latex_bash(),
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   652
                  "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }",
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   653
                  "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   654
                  latex_bash(),
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   655
                  latex_bash())
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   656
              }
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   657
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   658
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   659
            // result
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   660
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   661
            val root_pdf = Path.basic(root).pdf
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   662
            val result_path = doc_dir + root_pdf
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   663
72882
1dc2ad97e062 more informative error;
wenzelm
parents: 72880
diff changeset
   664
            val log_lines = result.out_lines ::: result.err_lines
1dc2ad97e062 more informative error;
wenzelm
parents: 72880
diff changeset
   665
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   666
            if (!result.ok) {
72882
1dc2ad97e062 more informative error;
wenzelm
parents: 72880
diff changeset
   667
              val message =
1dc2ad97e062 more informative error;
wenzelm
parents: 72880
diff changeset
   668
                Exn.cat_message(
1dc2ad97e062 more informative error;
wenzelm
parents: 72880
diff changeset
   669
                  Library.trim_line(result.err),
1dc2ad97e062 more informative error;
wenzelm
parents: 72880
diff changeset
   670
                  cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)),
1dc2ad97e062 more informative error;
wenzelm
parents: 72880
diff changeset
   671
                  "Failed to build document " + quote(doc.name))
1dc2ad97e062 more informative error;
wenzelm
parents: 72880
diff changeset
   672
              throw new Build_Error(log_lines, message)
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   673
            }
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   674
            else if (!result_path.is_file) {
72882
1dc2ad97e062 more informative error;
wenzelm
parents: 72880
diff changeset
   675
              val message = "Bad document result: expected to find " + root_pdf
1dc2ad97e062 more informative error;
wenzelm
parents: 72880
diff changeset
   676
              throw new Build_Error(log_lines, message)
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   677
            }
72665
7e5102e11c5e clarified messages;
wenzelm
parents: 72663
diff changeset
   678
            else {
7e5102e11c5e clarified messages;
wenzelm
parents: 72663
diff changeset
   679
              val stop = Time.now()
7e5102e11c5e clarified messages;
wenzelm
parents: 72663
diff changeset
   680
              val timing = stop - start
72699
ed59a506998f clarified document_output vs. progress;
wenzelm
parents: 72696
diff changeset
   681
              progress.echo("Finished " + session + "/" + doc.name +
72665
7e5102e11c5e clarified messages;
wenzelm
parents: 72663
diff changeset
   682
                " (" + timing.message_hms + " elapsed time)")
7e5102e11c5e clarified messages;
wenzelm
parents: 72663
diff changeset
   683
72882
1dc2ad97e062 more informative error;
wenzelm
parents: 72880
diff changeset
   684
              val log_xz = Bytes(cat_lines(log_lines)).compress()
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   685
              val pdf = Bytes.read(result_path)
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   686
              Document_Output(doc.name, sources, log_xz, pdf)
72665
7e5102e11c5e clarified messages;
wenzelm
parents: 72663
diff changeset
   687
            }
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   688
          }
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   689
        })
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   690
      }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   691
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   692
    for (dir <- output_pdf; doc <- documents) {
72675
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   693
      Isabelle_System.make_directory(dir)
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   694
      val path = dir + doc.path.pdf
72696
7af210f1f13b clarified signature and database layout;
wenzelm
parents: 72695
diff changeset
   695
      Bytes.write(path, doc.pdf)
72699
ed59a506998f clarified document_output vs. progress;
wenzelm
parents: 72696
diff changeset
   696
      progress.echo("Document at " + path.absolute)
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   697
    }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   698
72649
4ba5b1b08dd5 clarified signature: more explicit types;
wenzelm
parents: 72648
diff changeset
   699
    documents
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   700
  }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   701
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   702
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   703
  /* Isabelle tool wrapper */
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   704
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   705
  val isabelle_tool =
72763
3cc73d00553c added document antiquotation @{tool};
wenzelm
parents: 72723
diff changeset
   706
    Isabelle_Tool("document", "prepare session theory document", Scala_Project.here, args =>
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   707
    {
72675
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   708
      var output_sources: Option[Path] = None
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   709
      var output_pdf: Option[Path] = None
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   710
      var verbose_latex = false
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   711
      var dirs: List[Path] = Nil
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   712
      var options = Options.init()
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   713
      var verbose_build = false
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   714
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   715
      val getopts = Getopts(
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   716
        """
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   717
Usage: isabelle document [OPTIONS] SESSION
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   718
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   719
  Options are:
72675
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   720
    -O DIR       output directory for LaTeX sources and resulting PDF
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   721
    -P DIR       output directory for resulting PDF
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   722
    -S DIR       output directory for LaTeX sources
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   723
    -V           verbose latex
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   724
    -d DIR       include session directory
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   725
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   726
    -v           verbose build
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   727
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   728
  Prepare the theory document of a session.
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   729
""",
72675
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   730
        "O:" -> (arg =>
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   731
          {
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   732
            val dir = Path.explode(arg)
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   733
            output_sources = Some(dir)
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   734
            output_pdf = Some(dir)
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   735
          }),
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   736
        "P:" -> (arg => { output_pdf = Some(Path.explode(arg)) }),
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   737
        "S:" -> (arg => { output_sources = Some(Path.explode(arg)) }),
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   738
        "V" -> (_ => verbose_latex = true),
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   739
        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   740
        "o:" -> (arg => options = options + arg),
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   741
        "v" -> (_ => verbose_build = true))
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   742
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   743
      val more_args = getopts(args)
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   744
      val session =
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   745
        more_args match {
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   746
          case List(a) => a
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   747
          case _ => getopts.usage()
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   748
        }
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   749
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   750
      val progress = new Console_Progress(verbose = verbose_build)
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   751
      val store = Sessions.store(options)
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   752
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   753
      progress.interrupt_handler {
72650
787ba1d19d3a more robust: ensure coherence wrt. build database;
wenzelm
parents: 72649
diff changeset
   754
        val res =
787ba1d19d3a more robust: ensure coherence wrt. build database;
wenzelm
parents: 72649
diff changeset
   755
          Build.build(options, selection = Sessions.Selection.session(session),
787ba1d19d3a more robust: ensure coherence wrt. build database;
wenzelm
parents: 72649
diff changeset
   756
            dirs = dirs, progress = progress, verbose = verbose_build)
787ba1d19d3a more robust: ensure coherence wrt. build database;
wenzelm
parents: 72649
diff changeset
   757
        if (!res.ok) error("Failed to build session " + quote(session))
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   758
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   759
        val deps =
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   760
          Sessions.load_structure(options + "document=pdf", dirs = dirs).
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   761
            selection_deps(Sessions.Selection.session(session))
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   762
72675
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   763
        if (output_sources.isEmpty && output_pdf.isEmpty) {
cc1347c8c804 clarified document output;
wenzelm
parents: 72673
diff changeset
   764
          progress.echo_warning("No output directory")
72653
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   765
        }
ea35afdb1366 store documents within session database, instead of browser_info directory;
wenzelm
parents: 72652
diff changeset
   766
72854
6c660f05f70c clarified signature;
wenzelm
parents: 72847
diff changeset
   767
        using(store.open_database_context())(db_context =>
72683
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   768
          build_documents(session, deps, db_context, progress = progress,
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   769
            output_sources = output_sources, output_pdf = output_pdf,
b5e6f0d137a7 clarified signature: prefer Database_Context;
wenzelm
parents: 72682
diff changeset
   770
            verbose = true, verbose_latex = verbose_latex))
72574
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   771
      }
d892f6d66402 build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents: 72565
diff changeset
   772
    })
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
   773
}