src/Pure/Thy/present.scala
author wenzelm
Sun, 10 Dec 2017 18:31:41 +0100
changeset 67176 13b5c3ff1954
parent 66075 408a5325379c
child 67177 af5b89bc065c
permissions -rw-r--r--
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
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
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   104
  /* theory document */
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   105
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   106
  private val document_span_elements =
66075
408a5325379c tuned rendering;
wenzelm
parents: 66044
diff changeset
   107
    Rendering.foreground_elements ++ Rendering.text_color_elements + Markup.NUMERAL + Markup.COMMENT
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   108
66075
408a5325379c tuned rendering;
wenzelm
parents: 66044
diff changeset
   109
  private def make_html(xml: XML.Body): XML.Body =
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   110
    xml map {
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   111
      case XML.Wrapped_Elem(markup, body1, body2) =>
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   112
        XML.Wrapped_Elem(markup, make_html(body1), make_html(body2))
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   113
      case XML.Elem(markup, body) =>
66044
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   114
        val name = markup.name
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   115
        val html =
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   116
          markup.properties match {
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   117
            case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   118
              List(HTML.span(kind, make_html(body)))
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   119
            case _ =>
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   120
              make_html(body)
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   121
          }
66075
408a5325379c tuned rendering;
wenzelm
parents: 66044
diff changeset
   122
        Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
408a5325379c tuned rendering;
wenzelm
parents: 66044
diff changeset
   123
          case Some(c) => HTML.span(c.toString, html)
408a5325379c tuned rendering;
wenzelm
parents: 66044
diff changeset
   124
          case None => HTML.span(name, html)
66044
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   125
        }
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   126
      case XML.Text(text) =>
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   127
        XML.Text(Symbol.decode(text))
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   128
    }
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   129
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   130
  def theory_document(snapshot: Document.Snapshot): XML.Body =
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   131
  {
66043
f704c063e95d tuned signature;
wenzelm
parents: 66041
diff changeset
   132
    make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements))
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   133
  }
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   134
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   135
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   136
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   137
  /** build document **/
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   138
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   139
  val default_document_name = "document"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   140
  val default_document_format = "pdf"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   141
  val document_formats = List("pdf", "dvi")
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   142
  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
   143
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   144
  def document_tags(tags: List[String]): String =
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   145
  {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   146
    cat_lines(
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   147
      tags.map(tag =>
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   148
        tag.toList match {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   149
          case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   150
          case '-' :: cs => "\\isadroptag{" + cs.mkString + "}"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   151
          case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   152
          case cs => "\\isafoldtag{" + cs.mkString + "}"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   153
        })) + "\n"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   154
  }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   155
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   156
  def build_document(
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   157
    document_name: String = default_document_name,
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   158
    document_format: String = default_document_format,
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   159
    document_dir: Option[Path] = None,
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   160
    clean: Boolean = false,
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   161
    tags: List[String] = Nil)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   162
  {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   163
    if (!document_formats.contains(document_format))
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   164
      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
   165
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   166
    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
   167
    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
   168
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   169
    val root_name =
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   170
    {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   171
      val root1 = "root_" + document_name
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   172
      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
   173
    }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   174
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   175
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   176
    /* bash scripts */
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   177
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   178
    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
   179
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   180
    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
   181
      "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
   182
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   183
    def bash(script: String): Process_Result =
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   184
    {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   185
      Output.writeln(script)  // FIXME
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   186
      Isabelle_System.bash(script, cwd = dir.file)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   187
    }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   188
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   189
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   190
    /* clean target */
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   191
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   192
    val document_target = Path.parent + Path.explode(document_name).ext(document_format)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   193
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   194
    if (clean) {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   195
      bash("rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log " +
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   196
        File.bash_path(document_target)).check
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
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
    /* prepare document */
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   201
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   202
    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
   203
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   204
    val result =
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   205
      if ((dir + Path.explode("build")).is_file) {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   206
        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
   207
      }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   208
      else {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   209
        bash(
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   210
          List(
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   211
            latex_bash("sty"),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   212
            latex_bash(document_format),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   213
            "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }",
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   214
            "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   215
            latex_bash(document_format),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   216
            latex_bash(document_format)).mkString(" && "))
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   217
      }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   218
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   219
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   220
    /* result */
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   221
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   222
    if (!result.ok) {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   223
      cat_error(cat_lines(Latex.latex_errors(dir, root_name)),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   224
        "Document preparation failure in directory " + dir)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   225
    }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   226
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   227
    bash("[ -f " + root_bash(document_format) + " ] && cp -f " +
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   228
      root_bash(document_format) + " " + File.bash_path(document_target)).check
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   229
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   230
    // beware!
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   231
    if (clean) Isabelle_System.rm_tree(dir)
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
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   234
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   235
  /* Isabelle tool wrapper */
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
  val isabelle_tool =
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   238
    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
   239
  {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   240
    var clean = false
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   241
    var document_dir: Option[Path] = None
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   242
    var document_name = default_document_name
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   243
    var document_format = default_document_format
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   244
    var tags: List[String] = Nil
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   245
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   246
    val getopts = Getopts("""
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   247
Usage: isabelle document [OPTIONS]
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
  Options are:
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   250
    -c           aggressive cleanup of -d DIR content
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   251
    -d DIR       document output directory (default """ +
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   252
      default_document_dir(default_document_name) + """)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   253
    -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
   254
    -o FORMAT    document format: """ +
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   255
      commas(document_formats.map(fmt =>
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   256
        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
   257
    -t TAGS      markup for tagged regions
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
  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
   260
  specified output format.
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   261
""",
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   262
      "c" -> (_ => clean = true),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   263
      "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
   264
      "n:" -> (arg => document_name = arg),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   265
      "o:" -> (arg => document_format = arg),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   266
      "t:" -> (arg => tags = space_explode(',', arg)))
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   267
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   268
    val more_args = getopts(args)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   269
    if (more_args.nonEmpty) getopts.usage()
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
    build_document(document_dir = document_dir, document_name = document_name,
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   272
      document_format = document_format, clean = clean, tags = tags)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   273
  })
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
   274
}