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;
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@51402
    10
import scala.collection.immutable.SortedMap
wenzelm@51402
    11
wenzelm@51402
    12
wenzelm@50707
    13
object Present
wenzelm@50707
    14
{
wenzelm@51399
    15
  /* maintain chapter index -- NOT thread-safe */
wenzelm@50707
    16
wenzelm@50707
    17
  private val index_path = Path.basic("index.html")
wenzelm@51399
    18
  private val sessions_path = Path.basic(".sessions")
wenzelm@50707
    19
wenzelm@51402
    20
  private def read_sessions(dir: Path): List[(String, String)] =
wenzelm@51402
    21
  {
wenzelm@51416
    22
    val path = dir + sessions_path
wenzelm@51416
    23
    if (path.is_file) {
wenzelm@51416
    24
      import XML.Decode._
wenzelm@51416
    25
      list(pair(string, string))(YXML.parse_body(File.read(path)))
wenzelm@51416
    26
    }
wenzelm@51416
    27
    else Nil
wenzelm@51402
    28
  }
wenzelm@50707
    29
wenzelm@51402
    30
  private def write_sessions(dir: Path, sessions: List[(String, String)])
wenzelm@51402
    31
  {
wenzelm@51402
    32
    import XML.Encode._
wenzelm@51402
    33
    File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions)))
wenzelm@51402
    34
  }
wenzelm@50707
    35
wenzelm@51402
    36
  def update_chapter_index(info_path: Path, chapter: String, new_sessions: List[(String, String)])
wenzelm@51399
    37
  {
wenzelm@51399
    38
    val dir = info_path + Path.basic(chapter)
wenzelm@51399
    39
    Isabelle_System.mkdirs(dir)
wenzelm@50707
    40
wenzelm@51399
    41
    val sessions0 =
wenzelm@51406
    42
      try { read_sessions(dir) }
wenzelm@51987
    43
      catch { case _: XML.Error => Nil }
wenzelm@51399
    44
wenzelm@51402
    45
    val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
wenzelm@51402
    46
wenzelm@51399
    47
    write_sessions(dir, sessions)
wenzelm@51399
    48
    File.write(dir + index_path, HTML.chapter_index(chapter, sessions))
wenzelm@51399
    49
  }
wenzelm@50707
    50
}
wenzelm@50707
    51