src/Pure/Admin/afp.scala

--- a/src/Pure/Admin/afp.scala	Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Pure/Admin/afp.scala	Fri Apr 01 17:06:10 2022 +0200
@@ -11,8 +11,7 @@
 import scala.collection.immutable.SortedMap
 
 
-object AFP
-{
+object AFP {
   val groups: Map[String, String] =
     Map("large" -> "full 64-bit memory model or word arithmetic required",
       "slow" -> "CPU time much higher than 60min (on mid-range hardware)",
@@ -30,16 +29,14 @@
 
   /* entries */
 
-  def parse_date(s: String): Date =
-  {
+  def parse_date(s: String): Date = {
     val t = Date.Formatter.pattern("uuuu-MM-dd").parse(s)
     Date(LocalDate.from(t).atStartOfDay(Date.timezone_berlin))
   }
 
   def trim_mail(s: String): String = s.replaceAll("<[^>]*>", "").trim
 
-  sealed case class Entry(name: String, metadata: Properties.T, sessions: List[String])
-  {
+  sealed case class Entry(name: String, metadata: Properties.T, sessions: List[String]) {
     def get(prop: String): Option[String] = Properties.get(metadata, prop)
     def get_string(prop: String): String = get(prop).getOrElse("")
     def get_strings(prop: String): List[String] =
@@ -66,8 +63,7 @@
   }
 }
 
-class AFP private(options: Options, val base_dir: Path)
-{
+class AFP private(options: Options, val base_dir: Path) {
   override def toString: String = base_dir.expand.toString
 
   val main_dir: Path = base_dir + Path.explode("thys")
@@ -75,8 +71,7 @@
 
   /* metadata */
 
-  private val entry_metadata: Map[String, Properties.T] =
-  {
+  private val entry_metadata: Map[String, Properties.T] = {
     val metadata_file = base_dir + Path.explode("metadata/metadata")
 
     var result = Map.empty[String, Properties.T]
@@ -88,15 +83,13 @@
     val Extra_Line = """^\s+(.*)$""".r
     val Blank_Line = """^\s*$""".r
 
-    def flush(): Unit =
-    {
+    def flush(): Unit = {
       if (section != "") result += (section -> props.reverse.filter(p => p._2.nonEmpty))
       section = ""
       props = Nil
     }
 
-    for ((line, i) <- split_lines(File.read(metadata_file)).zipWithIndex)
-    {
+    for ((line, i) <- split_lines(File.read(metadata_file)).zipWithIndex) {
       def err(msg: String): Nothing =
         error(msg + Position.here(Position.Line_File(i + 1, metadata_file.expand.implode)))
 
@@ -122,8 +115,7 @@
 
   /* entries */
 
-  val entries_map: SortedMap[String, AFP.Entry] =
-  {
+  val entries_map: SortedMap[String, AFP.Entry] = {
     val entries =
       for (name <- Sessions.parse_roots(main_dir + Sessions.ROOTS)) yield {
         val metadata =
@@ -167,8 +159,7 @@
   private def sessions_deps(entry: AFP.Entry): List[String] =
     entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds).distinct.sorted
 
-  lazy val entries_graph: Graph[String, Unit] =
-  {
+  lazy val entries_graph: Graph[String, Unit] = {
     val session_entries =
       entries.foldLeft(Map.empty[String, String]) {
         case (m1, e) => e.sessions.foldLeft(m1) { case (m2, s) => m2 + (s -> e.name) }