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