diff --git a/admin/jenkins/ci_build_afp.scala b/admin/jenkins/ci_build_afp.scala
--- a/admin/jenkins/ci_build_afp.scala
+++ b/admin/jenkins/ci_build_afp.scala
@@ -1,46 +1,43 @@
-object profile extends isabelle.CI_Profile
-{
+object profile extends isabelle.CI_Profile {
   import isabelle._
   import java.io.FileReader
   import scala.sys.process._
   import org.apache.commons.configuration2._
 
   override def clean = false
 
   val afp = Path.explode("$ISABELLE_HOME/afp")
   val afp_thys = afp + Path.explode("thys")
   val afp_id = hg_id(afp)
 
   val status_file = Path.explode("$ISABELLE_HOME/status.json").file
   val deps_file = Path.explode("$ISABELLE_HOME/dependencies.json").file
   def can_send_mails = System.getProperties().containsKey("mail.smtp.host")
 
   def include = List(afp_thys)
   def select = Nil
 
-  def pre_hook(args: List[String]) =
-  {
+  def pre_hook(args: List[String]) = {
     println(s"AFP id $afp_id")
     if (status_file.exists())
       status_file.delete()
     Result.ok
   }
 
-  def post_hook(results: Build.Results) =
-  {
+  def post_hook(results: Build.Results) = {
     print_section("DEPENDENCIES")
     println("Generating dependencies file ...")
     val result = Isabelle_System.bash("isabelle afp_dependencies")
     result.check
     println("Writing dependencies file ...")
     File.write(deps_file, result.out)
     print_section("COMPLETED")
     Result.ok
   }
 
   def selection =
     Sessions.Selection(
       session_groups = List("AFP"),
       exclude_session_groups = List("slow"))
 
 }
diff --git a/admin/jenkins/ci_build_all.scala b/admin/jenkins/ci_build_all.scala
--- a/admin/jenkins/ci_build_all.scala
+++ b/admin/jenkins/ci_build_all.scala
@@ -1,275 +1,262 @@
-object profile extends isabelle.CI_Profile
-{
+object profile extends isabelle.CI_Profile {
   import isabelle._
   import java.io.FileReader
   import scala.sys.process._
   import org.apache.commons.configuration2._
 
   override def clean = false
 
   val afp = Path.explode("$AFP_BASE")
   val afp_thys = afp + Path.explode("thys")
   val afp_id = hg_id(afp)
 
-  sealed abstract class Status(val str: String)
-  {
+  sealed abstract class Status(val str: String) {
     def merge(that: Status): Status = (this, that) match {
       case (Ok, s) => s
       case (Failed, s) => Failed
       case (Skipped, Failed) => Failed
       case (Skipped, s) => Skipped
     }
   }
-  object Status
-  {
+  object Status {
     def merge(statuses: List[Status]): Status =
       statuses.foldLeft(Ok: Status)(_ merge _)
 
     def from_results(results: Build.Results, session: String): Status =
       if (results.cancelled(session))
         Skipped
       else if (results(session).ok)
         Ok
       else
         Failed
   }
 
   case object Ok extends Status("ok")
   case object Skipped extends Status("skipped")
   case object Failed extends Status("failed")
 
   case class Mail(subject: String, recipients: List[String], text: String) {
     import java.util._
     import javax.mail._
     import javax.mail.internet._
     import javax.activation._
 
     def send(): Unit = {
       val user = System.getProperty("mail.smtp.user")
       val sender = System.getProperty("mail.smtp.from")
       val password = System.getProperty("mail.smtp.password")
 
       System.setProperty("mail.smtp.ssl.protocols", "TLSv1.2")
 
       val authenticator = new Authenticator() {
         override def getPasswordAuthentication() =
           new PasswordAuthentication(user, password)
       }
 
       val session = Session.getDefaultInstance(System.getProperties(), authenticator)
       val message = new MimeMessage(session)
       message.setFrom(new InternetAddress("ci@isabelle.systems", "Isabelle/Jenkins"))
       message.setSender(new InternetAddress(sender))
       message.setSubject(subject)
       message.setText(text, "UTF-8")
       message.setSentDate(new java.util.Date())
 
       recipients.foreach { recipient =>
         message.addRecipient(Message.RecipientType.TO, new InternetAddress(recipient))
       }
 
       try {
         Transport.send(message)
       }
       catch {
         case ex: MessagingException => println(s"Sending mail failed: ${ex.getMessage}")
       }
     }
   }
 
-  class Metadata(ini: INIConfiguration)
-  {
+  class Metadata(ini: INIConfiguration) {
 
-    def maintainers(entry: String): List[String] =
-    {
+    def maintainers(entry: String): List[String] = {
       val config = ini.getSection(entry)
       val raw =
         if (config.containsKey("notify"))
           config.getString("notify")
         else
           ""
       List(raw.split(','): _*).map(_.trim).filterNot(_.isEmpty)
     }
 
-    def entry_of_session(info: Sessions.Info): Option[String] =
-    {
+    def entry_of_session(info: Sessions.Info): Option[String] = {
       val afp_path = afp_thys.canonical_file.toPath
       val session_path = info.dir.canonical_file.toPath
 
       if (session_path.startsWith(afp_path))
         Some(afp_path.relativize(session_path).getName(0).toFile.getName)
       else
         None
     }
 
     def notify(name: String, result: Process_Result, info: Sessions.Info): Unit =
       entry_of_session(info).foreach { entry =>
         val mails = maintainers(entry)
 
         val text =
           s"""|The build for the session
               |  $name,
               |belonging to the AFP entry
               |  $entry
               |failed.
               |
               |You are receiving this mail because you are the maintainer of that AFP
               |entry.
               |
               |The following information might help you with resolving the problem.
               |
               |Build log:    ${Isabelle_System.getenv("BUILD_URL")}
               |Isabelle ID:  $isabelle_id
               |AFP ID:       $afp_id
               |Timeout?      ${result.timeout}
               |Exit code:    ${result.rc}
               |
               |Last 50 lines from stdout (if available):
               |
               |${result.out_lines.takeRight(50).mkString("\n")}
               |
               |Last 50 lines from stderr (if available):
               |
               |${result.err_lines.takeRight(50).mkString("\n")}
               |""".stripMargin
 
         val subject = s"Build of AFP entry $entry failed"
 
         if (mails.isEmpty)
           println(s"Entry $entry: WARNING no maintainers specified")
         else
           Mail(text = text, subject = subject, recipients = mails).send()
       }
 
     def group_by_entry(results: Build.Results): Map[Option[String], List[String]] =
       results.sessions.toList.map { name =>
         entry_of_session(results.info(name)) -> name
       }.groupBy(_._1).view.mapValues(_.map(_._2)).toMap
 
-    def status_as_json(status: Map[Option[String], Status]): String =
-    {
+    def status_as_json(status: Map[Option[String], Status]): String = {
       val entries_strings = status.collect {
         case (Some(entry), status) =>
           s"""{"entry": "$entry", "status": "${status.str}"}"""
       }
 
       val entries_string = entries_strings.mkString("[", ",\n", "]")
 
       s"""
         {"build_data":
           {"isabelle_id": "$isabelle_id",
            "afp_id": "$afp_id",
            "time": "$start_time",
            "url": "${Isabelle_System.getenv("BUILD_URL")}",
            "job": "${Isabelle_System.getenv("JOB_NAME")}"
           },
          "entries":
            $entries_string
         }
       """
     }
 
-    def status_as_html(status: Map[Option[String], Status]): String =
-    {
+    def status_as_html(status: Map[Option[String], Status]): String = {
       val entries_strings = status.collect {
         case (None, Failed) =>
           s"<li>Distribution</li>"
         case (Some(entry), Failed) =>
           s"""<li><a href="https://devel.isa-afp.org/entries/$entry.html">$entry</a></li>"""
       }
 
       if (entries_strings.isEmpty)
         ""
       else
         entries_strings.mkString("Failed entries: <ul>", "\n", "</ul>")
     }
   }
 
   val status_file = Path.explode("$ISABELLE_HOME/status.json").file
   val report_file = Path.explode("$ISABELLE_HOME/report.html").file
   val deps_file = Path.explode("$ISABELLE_HOME/dependencies.json").file
   def can_send_mails = System.getProperties().containsKey("mail.smtp.host")
 
   def include = List(afp_thys)
   def select = Nil
 
-  def pre_hook(args: List[String]) =
-  {
+  def pre_hook(args: List[String]) = {
     println(s"AFP id $afp_id")
     if (status_file.exists())
       status_file.delete()
     if (report_file.exists())
       report_file.delete()
 
     File.write(report_file, "")
 
     if (!can_send_mails) {
       println(s"Mail configuration not found.")
       Result.error
     } else {
       Result.ok
     }
   }
 
-  def post_hook(results: Build.Results) =
-  {
+  def post_hook(results: Build.Results) = {
     print_section("DEPENDENCIES")
     println("Generating dependencies file ...")
     val result = Isabelle_System.bash("isabelle afp_dependencies")
     result.check
     println("Writing dependencies file ...")
     File.write(deps_file, result.out)
 
     val metadata = {
       val path = afp + Path.explode("metadata/metadata")
       val ini = new INIConfiguration()
       if (path.is_file) {
         val reader = new FileReader(path.file)
         ini.read(reader)
         reader.close()
       }
       new Metadata(ini)
     }
 
     val status =
       metadata.group_by_entry(results).view.mapValues { sessions =>
         Status.merge(sessions.map(Status.from_results(results, _)))
       }.toMap
 
     print_section("REPORT")
     println("Writing report file ...")
     File.write(report_file, metadata.status_as_html(status))
 
     print_section("SITEGEN")
     println("Writing status file ...")
     File.write(status_file, metadata.status_as_json(status))
     println("Running sitegen ...")
 
     val script = afp + Path.explode("admin/sitegen-devel")
     val sitegen_rc = List(script.file.toString, status_file.toString, deps_file.toString).!
-    if (sitegen_rc > 0)
-    {
+    if (sitegen_rc > 0) {
       println("sitegen failed")
     }
 
-    if (!results.ok)
-    {
+    if (!results.ok) {
       print_section("NOTIFICATIONS")
-      for (name <- results.sessions)
-      {
+      for (name <- results.sessions) {
         val result = results(name)
         if (!result.ok && !results.cancelled(name) && can_send_mails)
           metadata.notify(name, result, results.info(name))
       }
     }
 
     print_section("COMPLETED")
     Result(sitegen_rc)
   }
 
   def selection =
     Sessions.Selection(
       all_sessions = true,
       exclude_session_groups = List("slow"))
 
 }
diff --git a/admin/jenkins/ci_build_mac.scala b/admin/jenkins/ci_build_mac.scala
--- a/admin/jenkins/ci_build_mac.scala
+++ b/admin/jenkins/ci_build_mac.scala
@@ -1,27 +1,25 @@
-object profile extends isabelle.CI_Profile
-{
+object profile extends isabelle.CI_Profile {
 
   import isabelle._
 
   val afp = Path.explode("$ISABELLE_HOME/afp")
   val afp_thys = afp + Path.explode("thys")
 
   override def threads = 8
   override def jobs = 1
   def include = List(afp_thys)
   def select = Nil
 
-  def pre_hook(args: List[String]) =
-  {
+  def pre_hook(args: List[String]) = {
     println(s"Build for AFP id ${hg_id(afp)}")
     Result.ok
   }
 
   def post_hook(results: Build.Results) = Result.ok
 
   def selection = Sessions.Selection(
     all_sessions = true,
     exclude_sessions = List("HOL-Proofs", "HOL-ODE-Numerics", "Linear_Programming", "HOL-Nominal-Examples", "HOL-Analysis"),
     exclude_session_groups = List("slow"))
 
 }
diff --git a/admin/jenkins/ci_build_slow.scala b/admin/jenkins/ci_build_slow.scala
--- a/admin/jenkins/ci_build_slow.scala
+++ b/admin/jenkins/ci_build_slow.scala
@@ -1,24 +1,21 @@
-object profile extends isabelle.CI_Profile
-{
+object profile extends isabelle.CI_Profile {
 
   import isabelle._
 
   val afp = Path.explode("$ISABELLE_HOME/afp")
   val afp_thys = afp + Path.explode("thys")
 
   override def threads = 8
   override def jobs = 1
   def include = List(afp_thys)
   def select = Nil
 
-  def pre_hook(args: List[String]) =
-  {
+  def pre_hook(args: List[String]) = {
     println(s"Build for AFP id ${hg_id(afp)}")
     Result.ok
   }
 
   def post_hook(results: Build.Results) = Result.ok
 
   def selection = Sessions.Selection(session_groups = List("slow"))
-
 }
diff --git a/admin/jenkins/ci_build_testboard.scala b/admin/jenkins/ci_build_testboard.scala
--- a/admin/jenkins/ci_build_testboard.scala
+++ b/admin/jenkins/ci_build_testboard.scala
@@ -1,121 +1,113 @@
-object profile extends isabelle.CI_Profile
-{
+object profile extends isabelle.CI_Profile {
   import isabelle._
   import java.io.FileReader
   import scala.sys.process._
   import org.apache.commons.configuration2._
 
   override def clean = false
 
   val afp = Path.explode("$AFP_BASE")
   val afp_thys = afp + Path.explode("thys")
   val afp_id = hg_id(afp)
 
-  sealed abstract class Status(val str: String)
-  {
+  sealed abstract class Status(val str: String) {
     def merge(that: Status): Status = (this, that) match {
       case (Ok, s) => s
       case (Failed, s) => Failed
       case (Skipped, Failed) => Failed
       case (Skipped, s) => Skipped
     }
   }
-  object Status
-  {
+  object Status {
     def merge(statuses: List[Status]): Status =
       statuses.foldLeft(Ok: Status)(_ merge _)
 
     def from_results(results: Build.Results, session: String): Status =
       if (results.cancelled(session))
         Skipped
       else if (results(session).ok)
         Ok
       else
         Failed
   }
 
   case object Ok extends Status("ok")
   case object Skipped extends Status("skipped")
   case object Failed extends Status("failed")
 
-  class Metadata(ini: INIConfiguration)
-  {
+  class Metadata(ini: INIConfiguration) {
 
-    def entry_of_session(info: Sessions.Info): Option[String] =
-    {
+    def entry_of_session(info: Sessions.Info): Option[String] = {
       val afp_path = afp_thys.canonical_file.toPath
       val session_path = info.dir.canonical_file.toPath
 
       if (session_path.startsWith(afp_path))
         Some(afp_path.relativize(session_path).getName(0).toFile.getName)
       else
         None
     }
 
     def group_by_entry(results: Build.Results): Map[Option[String], List[String]] =
       results.sessions.toList.map { name =>
         entry_of_session(results.info(name)) -> name
       }.groupBy(_._1).view.mapValues(_.map(_._2)).toMap
 
-    def status_as_html(status: Map[Option[String], Status]): String =
-    {
+    def status_as_html(status: Map[Option[String], Status]): String = {
       val entries_strings = status.collect {
         case (None, Failed) =>
           s"<li>Distribution</li>"
         case (Some(entry), Failed) =>
           s"""<li><a href="https://devel.isa-afp.org/entries/$entry.html">$entry</a></li>"""
       }
 
       if (entries_strings.isEmpty)
         ""
       else
         entries_strings.mkString("Failed entries: <ul>", "\n", "</ul>")
     }
   }
 
   val report_file = Path.explode("$ISABELLE_HOME/report.html").file
 
   def include = List(afp_thys)
   def select = Nil
 
-  def pre_hook(args: List[String]) =
-  {
+  def pre_hook(args: List[String]) = {
     println(s"AFP id $afp_id")
     if (report_file.exists())
       report_file.delete()
 
     File.write(report_file, "")
     Result.ok
   }
 
-  def post_hook(results: Build.Results) =
-  {
+  def post_hook(results: Build.Results) = {
     val metadata = {
       val path = afp + Path.explode("metadata/metadata")
       val ini = new INIConfiguration()
       if (path.is_file) {
         val reader = new FileReader(path.file)
         ini.read(reader)
         reader.close()
       }
       new Metadata(ini)
     }
 
     val status =
       metadata.group_by_entry(results).view.mapValues { sessions =>
         Status.merge(sessions.map(Status.from_results(results, _)))
       }.toMap
 
     print_section("REPORT")
     println("Writing report file ...")
     File.write(report_file, metadata.status_as_html(status))
     print_section("COMPLETED")
     Result.ok
   }
 
   def selection =
     Sessions.Selection(
       all_sessions = true,
       exclude_session_groups = List("slow"))
 
 }
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,134 +1,131 @@
 // DESCRIPTION: check ROOT files of AFP sessions
 
 object AFP_Check_Roots extends isabelle.Isabelle_Tool.Body {
 
   import isabelle._
 
   val afp_dir = Path.explode("$AFP").expand
   val excludes = List("ROOTS", "LICENSE", "LICENSE.LGPL", ".DS_Store", "etc")
 
   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
       }
   }
 
   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
   )
 
-  def apply(args: List[String]): Unit =
-  {
+  def apply(args: 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 = List(
       check_timeout,
       // check_paths,
       check_chapter,
       check_groups,
       check_presence)
 
     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")
     }
   }
 
 }
diff --git a/tools/afp_dependencies.scala b/tools/afp_dependencies.scala
--- a/tools/afp_dependencies.scala
+++ b/tools/afp_dependencies.scala
@@ -1,44 +1,42 @@
 // DESCRIPTION: extract dependencies between AFP entries
 
 object AFP_Dependencies extends isabelle.Isabelle_Tool.Body {
 
   import isabelle._
 
   val afp_dir = Path.explode("$AFP").expand
 
   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] =
-  {
+  def get_entry(name: String): Option[String] = {
     val info = tree(name)
     val dir = info.dir
 
     if (dir.dir.expand.file != afp_dir.file)
       None
     else
       Some(dir.base.implode)
   }
 
   def as_json(entry: String, distrib_deps: List[String], afp_deps: List[String]): String =
     s"""
       {"$entry":
         {"distrib_deps": [${commas_quote(distrib_deps)}],
          "afp_deps": [${commas_quote(afp_deps)}]
         }
       }"""
 
-  def apply(args: List[String]): Unit =
-  {
+  def apply(args: List[String]): Unit = {
     val result = selected.groupBy(get_entry).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
         as_json(e, distrib_deps, afp_deps)
     }
 
     println("[" + commas(result) + "]")
   }
 
 }