some administrative support for AFP;
authorwenzelm
Mon, 09 Oct 2017 17:09:08 +0200
changeset 66820 fc516da7ee4f
parent 66819 064c80e9d1cf
child 66821 c0e8c199cb2e
some administrative support for AFP;
src/Pure/Admin/afp.scala
src/Pure/build-jars
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/afp.scala	Mon Oct 09 17:09:08 2017 +0200
@@ -0,0 +1,32 @@
+/*  Title:      Pure/Admin/afp.scala
+    Author:     Makarius
+
+Administrative support for the Archive of Formal Proofs.
+*/
+
+package isabelle
+
+
+object AFP
+{
+  sealed case class Entry(name: String, sessions: List[String])
+
+  def init(base_dir: Path = Path.explode("$AFP_BASE")): AFP = new AFP(base_dir)
+}
+
+class AFP private(val base_dir: Path)
+{
+  val main_dir: Path = base_dir + Path.explode("thys")
+
+  val entries: List[AFP.Entry] =
+    (for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS))
+    yield {
+      val sessions =
+        Sessions.parse_root_entries(main_dir + Path.explode(name) + Sessions.ROOT).map(_.name)
+      AFP.Entry(name, sessions)
+    }).sortBy(_.name)
+
+  val sessions: List[String] = entries.flatMap(_.sessions).sorted
+
+  override def toString: String = base_dir.expand.toString
+}
--- a/src/Pure/build-jars	Mon Oct 09 17:08:37 2017 +0200
+++ b/src/Pure/build-jars	Mon Oct 09 17:09:08 2017 +0200
@@ -9,6 +9,7 @@
 ## sources
 
 declare -a SOURCES=(
+  Admin/afp.scala
   Admin/build_cygwin.scala
   Admin/build_doc.scala
   Admin/build_history.scala