src/Pure/Thy/present.scala
author wenzelm
Sat, 28 Jul 2018 21:21:26 +0200
changeset 68704 71aa5a9128c2
parent 68132 2a5ae592eafb
child 69033 c5db368833b1
permissions -rw-r--r--
proper return code (true) if file is absent;
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
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
     4
Theory presentation: HTML.
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
61372
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    10
import java.io.{File => JFile}
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    11
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    12
import scala.collection.immutable.SortedMap
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    13
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    14
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
    15
object Present
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
    16
{
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    17
  /* maintain chapter index -- NOT thread-safe */
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
    18
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    19
  private val sessions_path = Path.basic(".sessions")
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
    20
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    21
  private def read_sessions(dir: Path): List[(String, String)] =
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    22
  {
51416
e2505a192a7c do not absorb I/O errors;
wenzelm
parents: 51406
diff changeset
    23
    val path = dir + sessions_path
e2505a192a7c do not absorb I/O errors;
wenzelm
parents: 51406
diff changeset
    24
    if (path.is_file) {
e2505a192a7c do not absorb I/O errors;
wenzelm
parents: 51406
diff changeset
    25
      import XML.Decode._
65344
b99283eed13c clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents: 65089
diff changeset
    26
      list(pair(string, string))(Symbol.decode_yxml(File.read(path)))
51416
e2505a192a7c do not absorb I/O errors;
wenzelm
parents: 51406
diff changeset
    27
    }
e2505a192a7c do not absorb I/O errors;
wenzelm
parents: 51406
diff changeset
    28
    else Nil
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    29
  }
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
    30
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    31
  private def write_sessions(dir: Path, sessions: List[(String, String)])
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    32
  {
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    33
    import XML.Encode._
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    34
    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
    35
  }
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
    36
61372
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    37
  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
    38
  {
61372
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    39
    val dir = browser_info + Path.basic(chapter)
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    40
    Isabelle_System.mkdirs(dir)
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
    41
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    42
    val sessions0 =
51406
950b897f95bb proper path -- I/O was hidden due to permissiveness;
wenzelm
parents: 51402
diff changeset
    43
      try { read_sessions(dir) }
51987
7d8e0e3c553b tuned signature;
wenzelm
parents: 51416
diff changeset
    44
      catch { case _: XML.Error => Nil }
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    45
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    46
    val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
65988
8040d2563593 modernized generated HTML;
wenzelm
parents: 65404
diff changeset
    47
    write_sessions(dir, sessions)
51402
b05cd411d3d3 include session description in chapter index;
wenzelm
parents: 51399
diff changeset
    48
65988
8040d2563593 modernized generated HTML;
wenzelm
parents: 65404
diff changeset
    49
    val title = "Isabelle/" + chapter + " sessions"
8040d2563593 modernized generated HTML;
wenzelm
parents: 65404
diff changeset
    50
    HTML.write_document(dir, "index.html",
8040d2563593 modernized generated HTML;
wenzelm
parents: 65404
diff changeset
    51
      List(HTML.title(title + " (" + Distribution.version + ")")),
8040d2563593 modernized generated HTML;
wenzelm
parents: 65404
diff changeset
    52
      HTML.chapter(title) ::
8040d2563593 modernized generated HTML;
wenzelm
parents: 65404
diff changeset
    53
       (if (sessions.isEmpty) Nil
8040d2563593 modernized generated HTML;
wenzelm
parents: 65404
diff changeset
    54
        else
65992
50daca61efd6 tuned signature;
wenzelm
parents: 65989
diff changeset
    55
          List(HTML.div("sessions",
50daca61efd6 tuned signature;
wenzelm
parents: 65989
diff changeset
    56
            List(HTML.description(
65988
8040d2563593 modernized generated HTML;
wenzelm
parents: 65404
diff changeset
    57
              sessions.map({ case (name, description) =>
65989
68cd15585f46 tuned layout;
wenzelm
parents: 65988
diff changeset
    58
                (List(HTML.link(name + "/index.html", HTML.text(name))),
68cd15585f46 tuned layout;
wenzelm
parents: 65988
diff changeset
    59
                  if (description == "") Nil
66038
36bf57d6c011 tuned layout (amending 8040d2563593);
wenzelm
parents: 66000
diff changeset
    60
                  else HTML.break ::: List(HTML.pre(HTML.text(description)))) })))))))
51399
6ac3c29a300e discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents: 50707
diff changeset
    61
  }
61372
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    62
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    63
  def make_global_index(browser_info: Path)
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    64
  {
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    65
    if (!(browser_info + Path.explode("index.html")).is_file) {
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    66
      Isabelle_System.mkdirs(browser_info)
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    67
      File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    68
        browser_info + Path.explode("isabelle.gif"))
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    69
      File.write(browser_info + Path.explode("index.html"),
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    70
        File.read(Path.explode("~~/lib/html/library_index_header.template")) +
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    71
        File.read(Path.explode("~~/lib/html/library_index_content.template")) +
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    72
        File.read(Path.explode("~~/lib/html/library_index_footer.template")))
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    73
    }
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    74
  }
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    75
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    76
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    77
  /* finish session */
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    78
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    79
  def finish(
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    80
    progress: Progress,
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    81
    browser_info: Path,
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    82
    graph_file: JFile,
62631
c39614ddb80b clarified modules;
wenzelm
parents: 61500
diff changeset
    83
    info: Sessions.Info,
61372
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    84
    name: String)
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    85
  {
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    86
    val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name)
65089
1d219d76873b clarified fonts;
wenzelm
parents: 65083
diff changeset
    87
    val session_fonts = session_prefix + Path.explode("fonts")
61372
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    88
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
    89
    if (info.options.bool("browser_info")) {
65089
1d219d76873b clarified fonts;
wenzelm
parents: 65083
diff changeset
    90
      Isabelle_System.mkdirs(session_fonts)
62971
087e36ce0593 back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents: 62631
diff changeset
    91
087e36ce0593 back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents: 62631
diff changeset
    92
      val session_graph = session_prefix + Path.basic("session_graph.pdf")
087e36ce0593 back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents: 62631
diff changeset
    93
      File.copy(graph_file, session_graph.file)
087e36ce0593 back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents: 62631
diff changeset
    94
      Isabelle_System.bash("chmod a+r " + File.bash_path(session_graph))
087e36ce0593 back to exact copy of non-text file (amending dcc8e1d34b18);
wenzelm
parents: 62631
diff changeset
    95
66000
58aa6749ff36 generate CSS for Isabelle fonts;
wenzelm
parents: 65998
diff changeset
    96
      HTML.write_isabelle_css(session_prefix)
61500
56a167b31a7f Isabelle fonts via external component;
wenzelm
parents: 61484
diff changeset
    97
65083
wenzelm
parents: 63683
diff changeset
    98
      for (font <- Isabelle_System.fonts(html = true))
65089
1d219d76873b clarified fonts;
wenzelm
parents: 65083
diff changeset
    99
        File.copy(font, session_fonts)
61372
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   100
    }
cf40b6b1de54 more Present operations on Scala side;
wenzelm
parents: 60077
diff changeset
   101
  }
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   102
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   103
67253
93b4333f33bb clarified modules;
wenzelm
parents: 67251
diff changeset
   104
  /** preview **/
93b4333f33bb clarified modules;
wenzelm
parents: 67251
diff changeset
   105
67260
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   106
  sealed case class Preview(title: String, content: String)
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   107
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   108
  def preview(snapshot: Document.Snapshot,
67262
46540a2ead4b action "isabelle.draft" for plain-text preview;
wenzelm
parents: 67260
diff changeset
   109
    plain_text: Boolean = false,
67260
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   110
    fonts_url: String => String = HTML.fonts_url()): Preview =
67253
93b4333f33bb clarified modules;
wenzelm
parents: 67251
diff changeset
   111
  {
93b4333f33bb clarified modules;
wenzelm
parents: 67251
diff changeset
   112
    require(!snapshot.is_outdated)
93b4333f33bb clarified modules;
wenzelm
parents: 67251
diff changeset
   113
67264
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   114
    def output_document(title: String, body: XML.Body): String =
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   115
      HTML.output_document(
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   116
        List(
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   117
          HTML.style(HTML.fonts_css(fonts_url) + File.read(HTML.isabelle_css)),
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   118
          HTML.title(title)),
67337
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   119
        List(HTML.source(body)), css = "", structural = false)
67264
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   120
67253
93b4333f33bb clarified modules;
wenzelm
parents: 67251
diff changeset
   121
    val name = snapshot.node_name
67264
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   122
    if (plain_text) {
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   123
      val title = "File " + quote(name.path.base_name)
67265
f32287c95432 store full blob source for the sake of markup_to_XML;
wenzelm
parents: 67264
diff changeset
   124
      val content = output_document(title, HTML.text(snapshot.node.source))
67264
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   125
      Preview(title, content)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   126
    }
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   127
    else if (name.is_bibtex) {
67256
ce7d856680d1 proper title;
wenzelm
parents: 67253
diff changeset
   128
      val title = "Bibliography " + quote(name.path.base_name)
67260
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   129
      val content =
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   130
        Isabelle_System.with_tmp_file("bib", "bib") { bib =>
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   131
          File.write(bib, snapshot.node.source)
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   132
          Bibtex.html_output(List(bib), style = "unsort", title = title)
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   133
        }
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   134
      Preview(title, content)
67256
ce7d856680d1 proper title;
wenzelm
parents: 67253
diff changeset
   135
    }
67253
93b4333f33bb clarified modules;
wenzelm
parents: 67251
diff changeset
   136
    else {
67264
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   137
      val title =
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   138
        if (name.is_theory) "Theory " + quote(name.theory_base_name)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   139
        else "File " + quote(name.path.base_name)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   140
      val content = output_document(title, pide_document(snapshot))
67260
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   141
      Preview(title, content)
67253
93b4333f33bb clarified modules;
wenzelm
parents: 67251
diff changeset
   142
    }
93b4333f33bb clarified modules;
wenzelm
parents: 67251
diff changeset
   143
  }
93b4333f33bb clarified modules;
wenzelm
parents: 67251
diff changeset
   144
93b4333f33bb clarified modules;
wenzelm
parents: 67251
diff changeset
   145
67264
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   146
  /* PIDE document */
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   147
67336
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   148
  private val document_elements =
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   149
    Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements +
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   150
    Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   151
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   152
  private val div_elements =
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   153
    Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   154
      HTML.descr.name)
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   155
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   156
  private def html_div(html: XML.Body): Boolean =
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   157
    html exists {
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   158
      case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body)
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   159
      case XML.Text(_) => false
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   160
    }
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   161
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   162
  private def html_class(c: String, html: XML.Body): XML.Tree =
67337
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   163
    if (html.forall(_ == HTML.no_text)) HTML.no_text
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   164
    else if (html_div(html)) HTML.div(c, html)
4254cfd15b00 more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents: 67336
diff changeset
   165
    else HTML.span(c, html)
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   166
66075
408a5325379c tuned rendering;
wenzelm
parents: 66044
diff changeset
   167
  private def make_html(xml: XML.Body): XML.Body =
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   168
    xml map {
67336
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   169
      case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) =>
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   170
        html_class(Markup.Language.DOCUMENT, make_html(body))
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   171
      case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(make_html(body))
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   172
      case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(make_html(body))
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   173
      case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   174
      case XML.Elem(Markup.Markdown_List(kind), body) =>
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   175
        if (kind == Markup.ENUMERATE) HTML.enum(make_html(body)) else HTML.list(make_html(body))
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   176
      case XML.Elem(markup, body) =>
66044
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   177
        val name = markup.name
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   178
        val html =
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   179
          markup.properties match {
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   180
            case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
67336
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   181
              List(html_class(kind, make_html(body)))
66044
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   182
            case _ =>
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   183
              make_html(body)
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   184
          }
66075
408a5325379c tuned rendering;
wenzelm
parents: 66044
diff changeset
   185
        Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
67336
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   186
          case Some(c) => html_class(c.toString, html)
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   187
          case None => html_class(name, html)
66044
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   188
        }
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   189
      case XML.Text(text) =>
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   190
        XML.Text(Symbol.decode(text))
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   191
    }
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   192
67253
93b4333f33bb clarified modules;
wenzelm
parents: 67251
diff changeset
   193
  def pide_document(snapshot: Document.Snapshot): XML.Body =
67336
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67265
diff changeset
   194
    make_html(snapshot.markup_to_XML(Text.Range.full, document_elements))
67246
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67204
diff changeset
   195
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67204
diff changeset
   196
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   197
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   198
  /** build document **/
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   199
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   200
  val default_document_name = "document"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   201
  val default_document_format = "pdf"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   202
  val document_formats = List("pdf", "dvi")
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   203
  def default_document_dir(name: String): Path = Path.explode("output") + Path.basic(name)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   204
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   205
  def document_tags(tags: List[String]): String =
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   206
  {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   207
    cat_lines(
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   208
      tags.map(tag =>
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   209
        tag.toList match {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   210
          case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   211
          case '-' :: cs => "\\isadroptag{" + cs.mkString + "}"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   212
          case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
67201
4cffa4791ef7 proper \isakeeptag (amending 13b5c3ff1954);
wenzelm
parents: 67187
diff changeset
   213
          case cs => "\\isakeeptag{" + cs.mkString + "}"
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   214
        })) + "\n"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   215
  }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   216
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   217
  def build_document(
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   218
    document_name: String = default_document_name,
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   219
    document_format: String = default_document_format,
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   220
    document_dir: Option[Path] = None,
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   221
    tags: List[String] = Nil)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   222
  {
67177
af5b89bc065c removed obsolete option (see 74a1b722507e);
wenzelm
parents: 67176
diff changeset
   223
    val document_target = Path.parent + Path.explode(document_name).ext(document_format)
af5b89bc065c removed obsolete option (see 74a1b722507e);
wenzelm
parents: 67176
diff changeset
   224
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   225
    if (!document_formats.contains(document_format))
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   226
      error("Bad document output format: " + quote(document_format))
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   227
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   228
    val dir = document_dir getOrElse default_document_dir(document_name)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   229
    if (!dir.is_dir) error("Bad document output directory " + dir)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   230
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   231
    val root_name =
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   232
    {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   233
      val root1 = "root_" + document_name
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   234
      if ((dir + Path.explode(root1).ext("tex")).is_file) root1 else "root"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   235
    }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   236
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   237
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   238
    /* bash scripts */
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   239
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   240
    def root_bash(ext: String): String = Bash.string(root_name + "." + ext)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   241
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   242
    def latex_bash(fmt: String, ext: String = "tex"): String =
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   243
      "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root_name + "." + ext)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   244
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   245
    def bash(script: String): Process_Result =
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   246
      Isabelle_System.bash(script, cwd = dir.file)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   247
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   248
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   249
    /* prepare document */
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   250
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   251
    File.write(dir + Path.explode("isabelletags.sty"), document_tags(tags))
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   252
67204
849a838f7e57 purge log files -- avoid old errors;
wenzelm
parents: 67203
diff changeset
   253
    List("log", "blg").foreach(ext => (dir + Path.explode(root_name).ext(ext)).file.delete)
849a838f7e57 purge log files -- avoid old errors;
wenzelm
parents: 67203
diff changeset
   254
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   255
    val result =
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   256
      if ((dir + Path.explode("build")).is_file) {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   257
        bash("./build " + Bash.string(document_format) + " " + Bash.string(document_name))
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   258
      }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   259
      else {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   260
        bash(
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   261
          List(
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   262
            latex_bash("sty"),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   263
            latex_bash(document_format),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   264
            "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }",
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   265
            "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   266
            latex_bash(document_format),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   267
            latex_bash(document_format)).mkString(" && "))
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   268
      }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   269
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   270
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   271
    /* result */
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   272
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   273
    if (!result.ok) {
67203
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67201
diff changeset
   274
      cat_error(
68132
2a5ae592eafb more informative error, notably for missing executable;
wenzelm
parents: 67337
diff changeset
   275
        Library.trim_line(result.err),
67203
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67201
diff changeset
   276
        cat_lines(Latex.latex_errors(dir, root_name) ::: Bibtex.bibtex_errors(dir, root_name)),
67187
3457d7d43ee9 tuned message;
wenzelm
parents: 67180
diff changeset
   277
        "Failed to build document in " + File.path(dir.absolute_file))
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   278
    }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   279
68704
71aa5a9128c2 proper return code (true) if file is absent;
wenzelm
parents: 68132
diff changeset
   280
    bash("if [ -f " + root_bash(document_format) + " ]; then cp -f " +
71aa5a9128c2 proper return code (true) if file is absent;
wenzelm
parents: 68132
diff changeset
   281
      root_bash(document_format) + " " + File.bash_path(document_target) + "; fi").check
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   282
  }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   283
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   284
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   285
  /* Isabelle tool wrapper */
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   286
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   287
  val isabelle_tool =
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   288
    Isabelle_Tool("document", "prepare theory session document", args =>
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   289
  {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   290
    var document_dir: Option[Path] = None
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   291
    var document_name = default_document_name
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   292
    var document_format = default_document_format
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   293
    var tags: List[String] = Nil
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   294
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   295
    val getopts = Getopts("""
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   296
Usage: isabelle document [OPTIONS]
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   297
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   298
  Options are:
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   299
    -d DIR       document output directory (default """ +
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   300
      default_document_dir(default_document_name) + """)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   301
    -n NAME      document name (default """ + quote(default_document_name) + """)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   302
    -o FORMAT    document format: """ +
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   303
      commas(document_formats.map(fmt =>
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   304
        fmt + (if (fmt == default_document_format) " (default)" else ""))) + """
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   305
    -t TAGS      markup for tagged regions
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   306
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   307
  Prepare the theory session document in document directory, producing the
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   308
  specified output format.
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   309
""",
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   310
      "d:" -> (arg => document_dir = Some(Path.explode(arg))),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   311
      "n:" -> (arg => document_name = arg),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   312
      "o:" -> (arg => document_format = arg),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   313
      "t:" -> (arg => tags = space_explode(',', arg)))
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   314
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   315
    val more_args = getopts(args)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   316
    if (more_args.nonEmpty) getopts.usage()
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   317
67180
dcac4659d482 tuned messages;
wenzelm
parents: 67177
diff changeset
   318
    try {
dcac4659d482 tuned messages;
wenzelm
parents: 67177
diff changeset
   319
      build_document(document_dir = document_dir, document_name = document_name,
dcac4659d482 tuned messages;
wenzelm
parents: 67177
diff changeset
   320
        document_format = document_format, tags = tags)
dcac4659d482 tuned messages;
wenzelm
parents: 67177
diff changeset
   321
    }
dcac4659d482 tuned messages;
wenzelm
parents: 67177
diff changeset
   322
    catch { case ERROR(msg) => Output.writeln(msg); sys.exit(1) }
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   323
  })
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
   324
}