src/Pure/Thy/present.scala
author wenzelm
Wed Apr 15 15:27:45 2015 +0200 (2015-04-15)
changeset 60077 55cb9462e602
parent 51987 7d8e0e3c553b
child 61372 cf40b6b1de54
permissions -rw-r--r--
tuned signature, clarified modules;
     1 /*  Title:      Pure/Thy/present.scala
     2     Author:     Makarius
     3 
     4 Theory presentation: HTML.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.collection.immutable.SortedMap
    11 
    12 
    13 object Present
    14 {
    15   /* session graph */
    16 
    17   def session_graph(
    18     parent_session: String,
    19     parent_loaded: String => Boolean,
    20     deps: List[Thy_Info.Dep]): Graph_Display.Graph =
    21   {
    22     val parent_session_node =
    23       Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
    24 
    25     def node(name: Document.Node.Name): Graph_Display.Node =
    26       if (parent_loaded(name.theory)) parent_session_node
    27       else Graph_Display.Node(name.theory, "theory." + name.theory)
    28 
    29     (Graph_Display.empty_graph /: deps) {
    30       case (g, dep) =>
    31         if (parent_loaded(dep.name.theory)) g
    32         else {
    33           val a = node(dep.name)
    34           val bs = dep.header.imports.map({ case (name, _) => node(name) })
    35           ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
    36         }
    37     }
    38   }
    39 
    40 
    41   /* maintain chapter index -- NOT thread-safe */
    42 
    43   private val index_path = Path.basic("index.html")
    44   private val sessions_path = Path.basic(".sessions")
    45 
    46   private def read_sessions(dir: Path): List[(String, String)] =
    47   {
    48     val path = dir + sessions_path
    49     if (path.is_file) {
    50       import XML.Decode._
    51       list(pair(string, string))(YXML.parse_body(File.read(path)))
    52     }
    53     else Nil
    54   }
    55 
    56   private def write_sessions(dir: Path, sessions: List[(String, String)])
    57   {
    58     import XML.Encode._
    59     File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions)))
    60   }
    61 
    62   def update_chapter_index(info_path: Path, chapter: String, new_sessions: List[(String, String)])
    63   {
    64     val dir = info_path + Path.basic(chapter)
    65     Isabelle_System.mkdirs(dir)
    66 
    67     val sessions0 =
    68       try { read_sessions(dir) }
    69       catch { case _: XML.Error => Nil }
    70 
    71     val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
    72 
    73     write_sessions(dir, sessions)
    74     File.write(dir + index_path, HTML.chapter_index(chapter, sessions))
    75   }
    76 }