src/Pure/Admin/afp.scala
author wenzelm
Mon Oct 09 17:09:08 2017 +0200 (22 months ago)
changeset 66820 fc516da7ee4f
child 66821 c0e8c199cb2e
permissions -rw-r--r--
some administrative support for AFP;
     1 /*  Title:      Pure/Admin/afp.scala
     2     Author:     Makarius
     3 
     4 Administrative support for the Archive of Formal Proofs.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object AFP
    11 {
    12   sealed case class Entry(name: String, sessions: List[String])
    13 
    14   def init(base_dir: Path = Path.explode("$AFP_BASE")): AFP = new AFP(base_dir)
    15 }
    16 
    17 class AFP private(val base_dir: Path)
    18 {
    19   val main_dir: Path = base_dir + Path.explode("thys")
    20 
    21   val entries: List[AFP.Entry] =
    22     (for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS))
    23     yield {
    24       val sessions =
    25         Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name)
    26       AFP.Entry(name, sessions)
    27     }).sortBy(_.name)
    28 
    29   val sessions: List[String] = entries.flatMap(_.sessions).sorted
    30 
    31   override def toString: String = base_dir.expand.toString
    32 }