src/Pure/Thy/present.scala
author wenzelm
Sat Apr 01 19:17:15 2017 +0200 (2017-04-01)
changeset 65344 b99283eed13c
parent 65089 1d219d76873b
child 65376 4ad983094226
permissions -rw-r--r--
clarified YXML vs. symbol encoding: operate on whole message;
     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   /* session graph */
    18 
    19   def session_graph(
    20     parent_session: String,
    21     parent_loaded: String => Boolean,
    22     deps: List[Thy_Info.Dep]): Graph_Display.Graph =
    23   {
    24     val parent_session_node =
    25       Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
    26 
    27     def node(name: Document.Node.Name): Graph_Display.Node =
    28       if (parent_loaded(name.theory)) parent_session_node
    29       else Graph_Display.Node(name.theory, "theory." + name.theory)
    30 
    31     (Graph_Display.empty_graph /: deps) {
    32       case (g, dep) =>
    33         if (parent_loaded(dep.name.theory)) g
    34         else {
    35           val a = node(dep.name)
    36           val bs = dep.header.imports.map({ case (name, _) => node(name) })
    37           ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
    38         }
    39     }
    40   }
    41 
    42 
    43   /* maintain chapter index -- NOT thread-safe */
    44 
    45   private val index_path = Path.basic("index.html")
    46   private val sessions_path = Path.basic(".sessions")
    47 
    48   private def read_sessions(dir: Path): List[(String, String)] =
    49   {
    50     val path = dir + sessions_path
    51     if (path.is_file) {
    52       import XML.Decode._
    53       list(pair(string, string))(Symbol.decode_yxml(File.read(path)))
    54     }
    55     else Nil
    56   }
    57 
    58   private def write_sessions(dir: Path, sessions: List[(String, String)])
    59   {
    60     import XML.Encode._
    61     File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions)))
    62   }
    63 
    64   def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)])
    65   {
    66     val dir = browser_info + Path.basic(chapter)
    67     Isabelle_System.mkdirs(dir)
    68 
    69     val sessions0 =
    70       try { read_sessions(dir) }
    71       catch { case _: XML.Error => Nil }
    72 
    73     val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
    74 
    75     write_sessions(dir, sessions)
    76     File.write(dir + index_path, HTML.chapter_index(chapter, sessions))
    77   }
    78 
    79   def make_global_index(browser_info: Path)
    80   {
    81     if (!(browser_info + Path.explode("index.html")).is_file) {
    82       Isabelle_System.mkdirs(browser_info)
    83       File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
    84         browser_info + Path.explode("isabelle.gif"))
    85       File.write(browser_info + Path.explode("index.html"),
    86         File.read(Path.explode("~~/lib/html/library_index_header.template")) +
    87         File.read(Path.explode("~~/lib/html/library_index_content.template")) +
    88         File.read(Path.explode("~~/lib/html/library_index_footer.template")))
    89     }
    90   }
    91 
    92 
    93   /* finish session */
    94 
    95   def finish(
    96     progress: Progress,
    97     browser_info: Path,
    98     graph_file: JFile,
    99     info: Sessions.Info,
   100     name: String)
   101   {
   102     val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name)
   103     val session_fonts = session_prefix + Path.explode("fonts")
   104 
   105     if (info.options.bool("browser_info")) {
   106       Isabelle_System.mkdirs(session_fonts)
   107 
   108       val session_graph = session_prefix + Path.basic("session_graph.pdf")
   109       File.copy(graph_file, session_graph.file)
   110       Isabelle_System.bash("chmod a+r " + File.bash_path(session_graph))
   111 
   112       File.copy(Path.explode("~~/etc/isabelle.css"), session_prefix)
   113 
   114       for (font <- Isabelle_System.fonts(html = true))
   115         File.copy(font, session_fonts)
   116     }
   117   }
   118 }