diff --git a/tools/afp_check_roots.scala b/tools/afp_check_roots.scala
--- a/tools/afp_check_roots.scala
+++ b/tools/afp_check_roots.scala
@@ -1,170 +1,160 @@
 package afp
 
 
 import isabelle._
 
 
-object AFP_Check_Roots
-{
+object AFP_Check_Roots {
   def print_good(string: String): Unit =
     println(Console.BOLD + Console.GREEN + string + Console.RESET)
 
   def print_bad(string: String): Unit =
     println(Console.BOLD + Console.RED + string + Console.RESET)
 
   class Check[T](
     run: (Sessions.Structure, List[String]) => List[T],
     failure_msg: String,
-    failure_format: T => String)
-  {
+    failure_format: T => String
+  ) {
     def apply(tree: Sessions.Structure, selected: List[String]): Boolean =
       run(tree, selected) match {
         case Nil =>
           true
         case offenders =>
           print_bad(failure_msg)
           offenders.foreach(offender => println("  " + failure_format(offender)))
           false
       }
   }
 
   def afp_checks(afp_dir: Path, excludes: List[String]): List[Check[_]] = {
     val check_timeout = new Check[(String, List[String])](
       run = { (tree, selected) =>
         selected.flatMap { name =>
           val info = tree(name)
           val entry = info.dir.base.implode
           val timeout = info.options.real("timeout")
           if (timeout == 0 || timeout % 300 != 0)
             Some((entry, name))
           else
             None
         }.groupBy(_._1).view.mapValues(_.map(_._2)).toList
       },
       failure_msg = "The following entries contain sessions without timeouts or with timeouts not divisible by 300:",
       failure_format = {
         case (entry, sessions) => s"""$entry ${sessions.mkString("(", ", ", ")")}"""
       }
     )
 
     val check_paths = new Check[(String, Path)](
       run = { (tree, selected) =>
         selected.flatMap { name =>
           val info = tree(name)
           val dir = info.dir
           if (dir.dir.expand.file != afp_dir.file)
             Some((name, dir))
           else
             None
         }
       },
       failure_msg = "The following sessions are in the wrong directory:",
       failure_format = {
         case (session, dir) => s"""$session ($dir)"""
       }
     )
 
     val check_chapter = new Check[String](
       run = { (tree, selected) =>
         selected.flatMap { name =>
           val info = tree(name)
           val entry = info.dir.base.implode
           if (info.chapter != "AFP")
             Some(entry)
           else
             None
         }.distinct
       },
       failure_msg = "The following entries are not in the AFP chapter:",
       failure_format = identity
     )
 
     val check_groups = new Check[(String, List[String])](
       run = { (tree, selected) =>
         selected.flatMap { name =>
           val info = tree(name)
           if (!info.groups.toSet.subsetOf(AFP.groups.keySet + "AFP") ||
             !info.groups.contains("AFP"))
             Some((name, info.groups))
           else
             None
         }
       },
       failure_msg = "The following sessions have wrong groups:",
       failure_format = {
         case (session, groups) => s"""$session ${groups.mkString("{", ", ", "}")}"""
       }
     )
 
     val check_presence = new Check[String](
       run = { (tree, selected) =>
         val fs_entries = File.read_dir(afp_dir).filterNot(excludes.contains)
 
         fs_entries.flatMap { name =>
           if (!selected.contains(name) || tree(name).dir.base.implode != name)
             Some(name)
           else
             None
         }
       },
       failure_msg = "The following entries (according to the file system) are not registered in ROOTS, or registered in the wrong ROOT:",
       failure_format = identity
     )
 
     List(
       check_timeout,
       // check_paths,
       check_chapter,
       check_groups,
       check_presence)
   }
 
-  def afp_check_roots(afp_dir: Path, excludes: List[String]): Unit =
-  {
+  def afp_check_roots(afp_dir: Path, excludes: List[String]): Unit = {
     val full_tree = Sessions.load_structure(Options.init(), Nil, List(afp_dir))
     val selected = full_tree.build_selection(Sessions.Selection.empty)
     val checks = afp_checks(afp_dir, excludes)
 
     val bad = checks.exists(check => !check(full_tree, selected))
 
-    if (bad)
-    {
+    if (bad) {
       print_bad("Errors found.")
       System.exit(1)
     }
-    else
-    {
+    else {
       print_good(s"${selected.length} sessions have been checked")
       print_good(s"${checks.length} checks have found no errors")
     }
   }
 
-  val isabelle_tool =
-    Isabelle_Tool(
-      "afp_check_roots",
-      "check ROOT files of AFP sessions",
-      Scala_Project.here,
-      args => {
-        var excludes = List("ROOTS", "LICENSE", "LICENSE.LGPL", ".DS_Store", "etc")
+  val isabelle_tool = Isabelle_Tool("afp_check_roots", "check ROOT files of AFP sessions",
+    Scala_Project.here,
+    { args =>
+      var excludes = List("ROOTS", "LICENSE", "LICENSE.LGPL", ".DS_Store", "etc")
 
-        val getopts = Getopts(
-          """
+      val getopts = Getopts("""
 Usage: isabelle afp_check_roots [OPTIONS]
 
   Options are:
     -x NAME      exclude directories with name
                  (default """ + excludes.map(quote).mkString(", ") + """)
 
   Check ROOT files of AFP sessions.
 """,
-          "x:" -> (arg => excludes ::= arg)
-        )
-
-        getopts(args)
+        "x:" -> (arg => excludes ::= arg))
 
-        val afp_dir = Path.explode("$AFP").expand
+      getopts(args)
 
-        afp_check_roots(afp_dir, excludes)
-      }
-    )
+      val afp_dir = Path.explode("$AFP").expand
+
+      afp_check_roots(afp_dir, excludes)
+    })
 }
diff --git a/tools/afp_dependencies.scala b/tools/afp_dependencies.scala
--- a/tools/afp_dependencies.scala
+++ b/tools/afp_dependencies.scala
@@ -1,92 +1,86 @@
 /* Author: Fabian Huch, TU Muenchen
 
 Tool to extract dependencies of AFP entries.
  */
 package afp
 
 
 import Metadata.Entry
 
 
 import isabelle._
 
 
 object AFP_Dependencies {
   case class Dependency(entry: Entry.Name,  distrib_deps: List[Entry.Name], afp_deps: List[Entry.Name])
 
   object JSON {
     private def from_dep(dependency: Dependency): (String, isabelle.JSON.T) =
       dependency.entry ->
         isabelle.JSON.Object(
           "distrib_deps" -> dependency.distrib_deps,
           "afp_deps" -> dependency.afp_deps
         )
 
     def from_dependency(dep: Dependency): isabelle.JSON.T =
       isabelle.JSON.Object(from_dep(dep))
 
     def from_dependencies(deps: List[Dependency]): isabelle.JSON.T =
       deps.map(from_dep).toMap
   }
 
   def afp_dependencies(afp_dir: Path): List[Dependency] = {
     val tree = Sessions.load_structure(Options.init(), Nil, List(afp_dir))
     val selected = tree.selection(Sessions.Selection(false, false, Nil, Nil, Nil, Nil))
       .build_graph.keys
 
     def get_entry(name: String): Option[String] =
     {
       val info = tree(name)
       val dir = info.dir
 
       if (selected.contains(dir.dir.expand))
         None
       else
         Some(dir.base.implode)
     }
 
     selected.groupBy(get_entry).toList.collect {
       case (Some(e), sessions) =>
         val dependencies = sessions.flatMap(tree.imports_graph.imm_preds)
           .map(d => (d, get_entry(d)))
         val distrib_deps = dependencies.collect { case (d, None) => d }.distinct
         val afp_deps = dependencies.collect { case (_, Some(d)) if d != e => d }.distinct
         Dependency(e, distrib_deps, afp_deps)
     }
   }
 
-  val isabelle_tool =
-    Isabelle_Tool(
-      "afp_dependencies",
-      "extract dependencies between AFP entries",
-      Scala_Project.here,
-      args => {
-        var output_file: Option[Path] = None
+  val isabelle_tool = Isabelle_Tool("afp_dependencies", "extract dependencies between AFP entries",
+    Scala_Project.here,
+    { args =>
+      var output_file: Option[Path] = None
 
-        val getopts = Getopts(
-          """
+      val getopts = Getopts("""
 Usage: isabelle afp_dependencies [OPTIONS]
 
   Options are:
     -o FILE      output file name
 
   Extract dependencies between AFP entries.
 """,
-          "o:" -> (arg => output_file = Some(Path.explode(arg)))
-        )
-
-        getopts(args)
-        val afp_dir = Path.explode("$AFP").expand
-
-        val progress = new Console_Progress()
+        "o:" -> (arg => output_file = Some(Path.explode(arg))))
 
-        val res = afp_dependencies(afp_dir).map(JSON.from_dependency)
-        val json = isabelle.JSON.Format(res)
+      getopts(args)
+      val afp_dir = Path.explode("$AFP").expand
 
-        output_file match {
-          case Some(file) => File.write(file, json)
-          case None => progress.echo(json)
-        }
+      val progress = new Console_Progress()
+
+      val res = afp_dependencies(afp_dir).map(JSON.from_dependency)
+      val json = isabelle.JSON.Format(res)
+
+      output_file match {
+        case Some(file) => File.write(file, json)
+        case None => progress.echo(json)
       }
-    )
+    })
 }
diff --git a/tools/afp_structure.scala b/tools/afp_structure.scala
--- a/tools/afp_structure.scala
+++ b/tools/afp_structure.scala
@@ -1,123 +1,125 @@
 /* Author: Fabian Huch, TU Muenchen
 
 AFP Metadata file structure with save and load operations.
  */
 package afp
 
 
 import isabelle._
 
 
 class AFP_Structure private(val base_dir: Path) {
   /* files */
 
   val metadata_dir = base_dir + Path.basic("metadata")
 
   val thys_dir = base_dir + Path.basic("thys")
 
   private val authors_file = metadata_dir + Path.basic("authors.toml")
 
   private val releases_file = metadata_dir + Path.basic("releases.toml")
   
   private val licenses_file = metadata_dir + Path.basic("licenses.toml")
 
   private val topics_file = metadata_dir + Path.basic("topics.toml")
 
   private val entries_dir = metadata_dir + Path.basic("entries")
 
   private def entry_file(name: Metadata.Entry.Name): Path = entries_dir + Path.basic(name + ".toml")
 
 
   /* load */
 
   private def load[A](file: Path, parser: afp.TOML.T => A): A = {
     val content = File.read(file)
     val toml = TOML.parse(content)
     parser(toml)
   }
 
   def load_authors: List[Metadata.Author] = load(authors_file, Metadata.TOML.to_authors)
 
   def load_releases: List[Metadata.Release] = load(releases_file, Metadata.TOML.to_releases)
 
   def load_licenses: List[Metadata.License] = load(licenses_file, Metadata.TOML.to_licenses)
   
   def load_topics: List[Metadata.Topic] = load(topics_file, Metadata.TOML.to_topics)
 
   def load_entry(name: Metadata.Entry.Name,
     authors: Map[Metadata.Author.ID, Metadata.Author],
     topics: Map[Metadata.Topic.ID, Metadata.Topic],
     licenses: Map[Metadata.License.ID, Metadata.License],
     releases: Map[Metadata.Entry.Name, List[Metadata.Release]]
   ): Metadata.Entry = {
     val entry_releases = releases.getOrElse(name, error("No releases for entry " + name))
     load(entry_file(name), toml =>
       Metadata.TOML.to_entry(toml ++ TOML.T("name" -> name), authors, topics, licenses, entry_releases))
   }
 
   def load(): List[Metadata.Entry] = {
     val authors = load_authors.map(author => author.id -> author).toMap
-    val topics = load_topics.map(topic => topic.id -> topic).toMap
+    def sub_topics(topic: Metadata.Topic): List[Metadata.Topic] =
+      topic :: topic.sub_topics.flatMap(sub_topics)
+    val topics = Utils.grouped_sorted(load_topics.flatMap(sub_topics), (t: Metadata.Topic) => t.id)
     val licenses = load_licenses.map(license => license.id -> license).toMap
     val releases = load_releases.groupBy(_.entry)
     entries.map(name => load_entry(name, authors, topics, licenses, releases))
   }
 
 
   /* save */
 
   private def save(file: Path, content: afp.TOML.T): Unit = {
     file.file.mkdirs()
     File.write(file, TOML.Format(content))
   }
 
   def save_authors(authors: List[Metadata.Author]): Unit =
     save(authors_file, Metadata.TOML.from_authors(authors))
 
   def save_releases(releases: List[Metadata.Release]): Unit =
     save(releases_file, Metadata.TOML.from_releases(releases))
 
   def save_topics(topics: List[Metadata.Topic]): Unit =
     save(topics_file, Metadata.TOML.from_topics(topics))
 
   def save_entry(entry: Metadata.Entry): Unit =
     save(entry_file(entry.name), Metadata.TOML.from_entry(entry))
 
 
   /* sessions */
 
   def entries: List[Metadata.Entry.Name] = {
     val Entry = """([a-zA-Z0-9+_-]+)\.toml""".r
     val file_entries = File.read_dir(entries_dir).map {
       case Entry(name) => name
       case f => error("Unrecognized metadata entry: " + f)
     }
     val session_entries = Sessions.parse_roots(thys_dir + Path.basic("ROOTS"))
 
     val session_set = session_entries.toSet
     val metadata_set = file_entries.toSet
 
     if (session_set != metadata_set) {
       val inter = session_set.intersect(metadata_set)
       val session_without_metadata =
         if (session_set.subsetOf(inter)) ""
         else "No metadata for session roots: " + commas_quote(session_set -- inter)
       val metadata_without_session =
         if (metadata_set.subsetOf(inter)) ""
         else "Not session roots for metadata entries: " + commas_quote(metadata_set -- inter)
       error("Metadata does not match sessions:\n" + session_without_metadata + metadata_without_session)
     } else session_entries
   }
 
   def sessions_structure: Sessions.Structure =
     Sessions.load_structure(options = Options.init(), select_dirs = List(thys_dir))
 
   def entry_sessions(name: Metadata.Entry.Name): List[Sessions.Session_Entry] =
     Sessions.parse_root(thys_dir + Path.make(List(name, "ROOT"))).collect { case e: Sessions.Session_Entry => e }
 
   def hg_id: String = Mercurial.repository(base_dir).id()
 }
 
 object AFP_Structure {
   def apply(base_dir: Path = Path.explode("$AFP_BASE")): AFP_Structure = new AFP_Structure(base_dir.absolute)
 }