src/Pure/Thy/present.scala
author wenzelm
Tue Feb 11 17:44:29 2014 +0100 (2014-02-11)
changeset 55431 e0f20a44ff9d
parent 51987 7d8e0e3c553b
child 60077 55cb9462e602
permissions -rw-r--r--
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
more informative type Blob, to allow markup reports;
     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   /* maintain chapter index -- NOT thread-safe */
    16 
    17   private val index_path = Path.basic("index.html")
    18   private val sessions_path = Path.basic(".sessions")
    19 
    20   private def read_sessions(dir: Path): List[(String, String)] =
    21   {
    22     val path = dir + sessions_path
    23     if (path.is_file) {
    24       import XML.Decode._
    25       list(pair(string, string))(YXML.parse_body(File.read(path)))
    26     }
    27     else Nil
    28   }
    29 
    30   private def write_sessions(dir: Path, sessions: List[(String, String)])
    31   {
    32     import XML.Encode._
    33     File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions)))
    34   }
    35 
    36   def update_chapter_index(info_path: Path, chapter: String, new_sessions: List[(String, String)])
    37   {
    38     val dir = info_path + Path.basic(chapter)
    39     Isabelle_System.mkdirs(dir)
    40 
    41     val sessions0 =
    42       try { read_sessions(dir) }
    43       catch { case _: XML.Error => Nil }
    44 
    45     val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
    46 
    47     write_sessions(dir, sessions)
    48     File.write(dir + index_path, HTML.chapter_index(chapter, sessions))
    49   }
    50 }
    51