src/Pure/Thy/present.scala
author wenzelm
Thu, 08 Jun 2017 23:04:07 +0200
changeset 66044 bd7516709051
parent 66043 f704c063e95d
child 66075 408a5325379c
permissions -rw-r--r--
more HTML rendering as in Isabelle/jEdit; tuned;
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 =
66044
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   107
    Markup.Elements(Rendering.text_color.keySet + Markup.NUMERAL + Markup.COMMENT)
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   108
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   109
  def make_html(xml: XML.Body): XML.Body =
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
          }
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   122
        Rendering.text_color.get(name) match {
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   123
          case Some(c) =>
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   124
            HTML.span(c.toString, html)
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   125
          case None =>
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   126
            if (document_span_elements(name)) HTML.span(name, html)
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   127
            else XML.Elem(markup, html)
bd7516709051 more HTML rendering as in Isabelle/jEdit;
wenzelm
parents: 66043
diff changeset
   128
        }
66040
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   129
      case XML.Text(text) =>
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   130
        XML.Text(Symbol.decode(text))
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   131
    }
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   132
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   133
  def theory_document(snapshot: Document.Snapshot): XML.Body =
f826ba18fe08 HTML preview based on PIDE markup;
wenzelm
parents: 66038
diff changeset
   134
  {
66043
f704c063e95d tuned signature;
wenzelm
parents: 66041
diff changeset
   135
    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
   136
  }
50707
5b2bf7611662 maintain session index on Scala side, for more determistic results;
wenzelm
parents:
diff changeset
   137
}