src/Pure/Thy/present.scala
author wenzelm
Thu Jun 08 13:01:50 2017 +0200 (2017-06-08)
changeset 66038 36bf57d6c011
parent 66000 58aa6749ff36
child 66040 f826ba18fe08
permissions -rw-r--r--
tuned layout (amending 8040d2563593);
wenzelm@50707
     1
/*  Title:      Pure/Thy/present.scala
wenzelm@50707
     2
    Author:     Makarius
wenzelm@50707
     3
wenzelm@50707
     4
Theory presentation: HTML.
wenzelm@50707
     5
*/
wenzelm@50707
     6
wenzelm@50707
     7
package isabelle
wenzelm@50707
     8
wenzelm@50707
     9
wenzelm@61372
    10
import java.io.{File => JFile}
wenzelm@61372
    11
wenzelm@51402
    12
import scala.collection.immutable.SortedMap
wenzelm@51402
    13
wenzelm@51402
    14
wenzelm@50707
    15
object Present
wenzelm@50707
    16
{
wenzelm@51399
    17
  /* maintain chapter index -- NOT thread-safe */
wenzelm@50707
    18
wenzelm@51399
    19
  private val sessions_path = Path.basic(".sessions")
wenzelm@50707
    20
wenzelm@51402
    21
  private def read_sessions(dir: Path): List[(String, String)] =
wenzelm@51402
    22
  {
wenzelm@51416
    23
    val path = dir + sessions_path
wenzelm@51416
    24
    if (path.is_file) {
wenzelm@51416
    25
      import XML.Decode._
wenzelm@65344
    26
      list(pair(string, string))(Symbol.decode_yxml(File.read(path)))
wenzelm@51416
    27
    }
wenzelm@51416
    28
    else Nil
wenzelm@51402
    29
  }
wenzelm@50707
    30
wenzelm@51402
    31
  private def write_sessions(dir: Path, sessions: List[(String, String)])
wenzelm@51402
    32
  {
wenzelm@51402
    33
    import XML.Encode._
wenzelm@51402
    34
    File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions)))
wenzelm@51402
    35
  }
wenzelm@50707
    36
wenzelm@61372
    37
  def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)])
wenzelm@51399
    38
  {
wenzelm@61372
    39
    val dir = browser_info + Path.basic(chapter)
wenzelm@51399
    40
    Isabelle_System.mkdirs(dir)
wenzelm@50707
    41
wenzelm@51399
    42
    val sessions0 =
wenzelm@51406
    43
      try { read_sessions(dir) }
wenzelm@51987
    44
      catch { case _: XML.Error => Nil }
wenzelm@51399
    45
wenzelm@51402
    46
    val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
wenzelm@65988
    47
    write_sessions(dir, sessions)
wenzelm@51402
    48
wenzelm@65988
    49
    val title = "Isabelle/" + chapter + " sessions"
wenzelm@65988
    50
    HTML.write_document(dir, "index.html",
wenzelm@65988
    51
      List(HTML.title(title + " (" + Distribution.version + ")")),
wenzelm@65988
    52
      HTML.chapter(title) ::
wenzelm@65988
    53
       (if (sessions.isEmpty) Nil
wenzelm@65988
    54
        else
wenzelm@65992
    55
          List(HTML.div("sessions",
wenzelm@65992
    56
            List(HTML.description(
wenzelm@65988
    57
              sessions.map({ case (name, description) =>
wenzelm@65989
    58
                (List(HTML.link(name + "/index.html", HTML.text(name))),
wenzelm@65989
    59
                  if (description == "") Nil
wenzelm@66038
    60
                  else HTML.break ::: List(HTML.pre(HTML.text(description)))) })))))))
wenzelm@51399
    61
  }
wenzelm@61372
    62
wenzelm@61372
    63
  def make_global_index(browser_info: Path)
wenzelm@61372
    64
  {
wenzelm@61372
    65
    if (!(browser_info + Path.explode("index.html")).is_file) {
wenzelm@61372
    66
      Isabelle_System.mkdirs(browser_info)
wenzelm@61372
    67
      File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
wenzelm@61372
    68
        browser_info + Path.explode("isabelle.gif"))
wenzelm@61372
    69
      File.write(browser_info + Path.explode("index.html"),
wenzelm@61372
    70
        File.read(Path.explode("~~/lib/html/library_index_header.template")) +
wenzelm@61372
    71
        File.read(Path.explode("~~/lib/html/library_index_content.template")) +
wenzelm@61372
    72
        File.read(Path.explode("~~/lib/html/library_index_footer.template")))
wenzelm@61372
    73
    }
wenzelm@61372
    74
  }
wenzelm@61372
    75
wenzelm@61372
    76
wenzelm@61372
    77
  /* finish session */
wenzelm@61372
    78
wenzelm@61372
    79
  def finish(
wenzelm@61372
    80
    progress: Progress,
wenzelm@61372
    81
    browser_info: Path,
wenzelm@61372
    82
    graph_file: JFile,
wenzelm@62631
    83
    info: Sessions.Info,
wenzelm@61372
    84
    name: String)
wenzelm@61372
    85
  {
wenzelm@61372
    86
    val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name)
wenzelm@65089
    87
    val session_fonts = session_prefix + Path.explode("fonts")
wenzelm@61372
    88
wenzelm@61372
    89
    if (info.options.bool("browser_info")) {
wenzelm@65089
    90
      Isabelle_System.mkdirs(session_fonts)
wenzelm@62971
    91
wenzelm@62971
    92
      val session_graph = session_prefix + Path.basic("session_graph.pdf")
wenzelm@62971
    93
      File.copy(graph_file, session_graph.file)
wenzelm@62971
    94
      Isabelle_System.bash("chmod a+r " + File.bash_path(session_graph))
wenzelm@62971
    95
wenzelm@66000
    96
      HTML.write_isabelle_css(session_prefix)
wenzelm@61500
    97
wenzelm@65083
    98
      for (font <- Isabelle_System.fonts(html = true))
wenzelm@65089
    99
        File.copy(font, session_fonts)
wenzelm@61372
   100
    }
wenzelm@61372
   101
  }
wenzelm@50707
   102
}