src/Pure/Thy/present.scala
author wenzelm
Fri, 22 Dec 2017 20:15:16 +0100
changeset 67264 16f74b7c248a
parent 67262 46540a2ead4b
child 67265 f32287c95432
permissions -rw-r--r--
PIDE markup for non-theory nodes;
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)),
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   119
        List(HTML.source(body)), css = "")
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)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   124
      val source = Symbol.decode(snapshot.node.source)  // FIXME treat mixed encode/decode situation
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   125
      val content = output_document(title, HTML.text(source))
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   126
      Preview(title, content)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   127
    }
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   128
    else if (name.is_bibtex) {
67256
ce7d856680d1 proper title;
wenzelm
parents: 67253
diff changeset
   129
      val title = "Bibliography " + quote(name.path.base_name)
67260
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   130
      val content =
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   131
        Isabelle_System.with_tmp_file("bib", "bib") { bib =>
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   132
          File.write(bib, snapshot.node.source)
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   133
          Bibtex.html_output(List(bib), style = "unsort", title = title)
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   134
        }
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   135
      Preview(title, content)
67256
ce7d856680d1 proper title;
wenzelm
parents: 67253
diff changeset
   136
    }
67253
93b4333f33bb clarified modules;
wenzelm
parents: 67251
diff changeset
   137
    else {
67264
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   138
      val title =
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   139
        if (name.is_theory) "Theory " + quote(name.theory_base_name)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   140
        else "File " + quote(name.path.base_name)
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   141
      val content = output_document(title, pide_document(snapshot))
67260
ecd607631bc7 uniform preview for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 67256
diff changeset
   142
      Preview(title, content)
67253
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
93b4333f33bb clarified modules;
wenzelm
parents: 67251
diff changeset
   146
67264
16f74b7c248a PIDE markup for non-theory nodes;
wenzelm
parents: 67262
diff changeset
   147
  /* PIDE document */
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   148
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   149
  private val document_span_elements =
66075
408a5325379c tuned rendering;
wenzelm
parents: 66044
diff changeset
   150
    Rendering.foreground_elements ++ Rendering.text_color_elements + Markup.NUMERAL + Markup.COMMENT
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   151
66075
408a5325379c tuned rendering;
wenzelm
parents: 66044
diff changeset
   152
  private def make_html(xml: XML.Body): XML.Body =
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   153
    xml map {
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   154
      case XML.Wrapped_Elem(markup, body1, body2) =>
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   155
        XML.Wrapped_Elem(markup, make_html(body1), make_html(body2))
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   156
      case XML.Elem(markup, body) =>
66044
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   157
        val name = markup.name
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   158
        val html =
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   159
          markup.properties match {
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   160
            case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   161
              List(HTML.span(kind, make_html(body)))
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   162
            case _ =>
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   163
              make_html(body)
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   164
          }
66075
408a5325379c tuned rendering;
wenzelm
parents: 66044
diff changeset
   165
        Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
408a5325379c tuned rendering;
wenzelm
parents: 66044
diff changeset
   166
          case Some(c) => HTML.span(c.toString, html)
408a5325379c tuned rendering;
wenzelm
parents: 66044
diff changeset
   167
          case None => HTML.span(name, html)
66044
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   168
        }
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   169
      case XML.Text(text) =>
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   170
        XML.Text(Symbol.decode(text))
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   171
    }
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   172
67253
93b4333f33bb clarified modules;
wenzelm
parents: 67251
diff changeset
   173
  def pide_document(snapshot: Document.Snapshot): XML.Body =
67246
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67204
diff changeset
   174
    make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements))
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67204
diff changeset
   175
4cedf44f2af1 isabelle.preview presents auxiliary text files as well;
wenzelm
parents: 67204
diff changeset
   176
67176
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
  /** build document **/
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
  val default_document_name = "document"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   181
  val default_document_format = "pdf"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   182
  val document_formats = List("pdf", "dvi")
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   183
  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
   184
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   185
  def document_tags(tags: List[String]): String =
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   186
  {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   187
    cat_lines(
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   188
      tags.map(tag =>
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   189
        tag.toList match {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   190
          case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   191
          case '-' :: cs => "\\isadroptag{" + cs.mkString + "}"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   192
          case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
67201
4cffa4791ef7 proper \isakeeptag (amending 13b5c3ff1954);
wenzelm
parents: 67187
diff changeset
   193
          case cs => "\\isakeeptag{" + cs.mkString + "}"
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   194
        })) + "\n"
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   195
  }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   196
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   197
  def build_document(
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   198
    document_name: String = default_document_name,
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   199
    document_format: String = default_document_format,
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   200
    document_dir: Option[Path] = None,
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   201
    tags: List[String] = Nil)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   202
  {
67177
af5b89bc065c removed obsolete option (see 74a1b722507e);
wenzelm
parents: 67176
diff changeset
   203
    val document_target = Path.parent + Path.explode(document_name).ext(document_format)
af5b89bc065c removed obsolete option (see 74a1b722507e);
wenzelm
parents: 67176
diff changeset
   204
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   205
    if (!document_formats.contains(document_format))
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   206
      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
   207
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   208
    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
   209
    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
   210
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   211
    val root_name =
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   212
    {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   213
      val root1 = "root_" + document_name
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   214
      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
   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
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   218
    /* bash scripts */
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
    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
   221
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   222
    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
   223
      "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
   224
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   225
    def bash(script: String): Process_Result =
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   226
      Isabelle_System.bash(script, cwd = dir.file)
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
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   229
    /* prepare document */
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
    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
   232
67204
849a838f7e57 purge log files -- avoid old errors;
wenzelm
parents: 67203
diff changeset
   233
    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
   234
67176
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   235
    val result =
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   236
      if ((dir + Path.explode("build")).is_file) {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   237
        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
   238
      }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   239
      else {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   240
        bash(
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   241
          List(
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   242
            latex_bash("sty"),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   243
            latex_bash(document_format),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   244
            "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }",
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   245
            "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   246
            latex_bash(document_format),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   247
            latex_bash(document_format)).mkString(" && "))
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
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
    /* result */
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   252
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   253
    if (!result.ok) {
67203
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67201
diff changeset
   254
      cat_error(
85784e16bec8 expose bibtex errors;
wenzelm
parents: 67201
diff changeset
   255
        cat_lines(Latex.latex_errors(dir, root_name) ::: Bibtex.bibtex_errors(dir, root_name)),
67187
3457d7d43ee9 tuned message;
wenzelm
parents: 67180
diff changeset
   256
        "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
   257
    }
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
    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
   260
      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
   261
  }
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   262
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   263
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   264
  /* Isabelle tool wrapper */
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   265
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   266
  val isabelle_tool =
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   267
    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
   268
  {
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   269
    var document_dir: Option[Path] = None
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   270
    var document_name = default_document_name
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   271
    var document_format = default_document_format
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   272
    var tags: List[String] = Nil
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   273
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   274
    val getopts = Getopts("""
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   275
Usage: isabelle document [OPTIONS]
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   276
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   277
  Options are:
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   278
    -d DIR       document output directory (default """ +
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   279
      default_document_dir(default_document_name) + """)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   280
    -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
   281
    -o FORMAT    document format: """ +
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   282
      commas(document_formats.map(fmt =>
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   283
        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
   284
    -t TAGS      markup for tagged regions
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   285
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   286
  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
   287
  specified output format.
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   288
""",
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   289
      "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
   290
      "n:" -> (arg => document_name = arg),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   291
      "o:" -> (arg => document_format = arg),
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   292
      "t:" -> (arg => tags = space_explode(',', arg)))
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   293
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   294
    val more_args = getopts(args)
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   295
    if (more_args.nonEmpty) getopts.usage()
13b5c3ff1954 re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents: 66075
diff changeset
   296
67180
dcac4659d482 tuned messages;
wenzelm
parents: 67177
diff changeset
   297
    try {
dcac4659d482 tuned messages;
wenzelm
parents: 67177
diff changeset
   298
      build_document(document_dir = document_dir, document_name = document_name,
dcac4659d482 tuned messages;
wenzelm
parents: 67177
diff changeset
   299
        document_format = document_format, tags = tags)
dcac4659d482 tuned messages;
wenzelm
parents: 67177
diff changeset
   300
    }
dcac4659d482 tuned messages;
wenzelm
parents: 67177
diff changeset
   301
    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
   302
  })
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
   303
}