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