# HG changeset patch
# User wenzelm
# Date 1662233253 -7200
# Node ID 92aa9ac31c7c7da90b1c899d224b8885bb161505
# Parent  f244926013e5aeda232d3f7594634528debcbaa6
tuned --- more robust syntax;

diff -r f244926013e5 -r 92aa9ac31c7c src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Sep 03 17:37:46 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Sep 03 21:27:33 2022 +0200
@@ -193,8 +193,9 @@
 
             val imported_files = if (inlined_files) dependencies.imported_files else Nil
 
-            if (list_files)
+            if (list_files) {
               progress.echo(cat_lines(session_files.map(_.implode).sorted.map("  " + _)))
+            }
 
             if (check_keywords.nonEmpty) {
               Check_Keywords.check_keywords(
@@ -207,8 +208,9 @@
 
               def node(name: Document.Node.Name): Graph_Display.Node = {
                 val qualifier = sessions_structure.theory_qualifier(name)
-                if (qualifier == info.name)
+                if (qualifier == info.name) {
                   Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
+                }
                 else session_node(qualifier)
               }
 
@@ -590,9 +592,10 @@
         for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
         yield {
           val thy_name = Path.explode(thy).file_name
-          if (Long_Name.is_qualified(thy_name))
+          if (Long_Name.is_qualified(thy_name)) {
             error("Bad qualified name for global theory " +
               quote(thy_name) + Position.here(pos))
+          }
           else thy_name
         }
 
@@ -664,9 +667,10 @@
         edges: Info => Iterable[String]
       ) : Graph[String, Info] = {
         def add_edge(pos: Position.T, name: String, g: Graph[String, Info], parent: String) = {
-          if (!g.defined(parent))
+          if (!g.defined(parent)) {
             error("Bad " + kind + " session " + quote(parent) + " for " +
               quote(name) + Position.here(pos))
+          }
 
           try { g.add_edge_acyclic(parent, name) }
           catch {
@@ -685,9 +689,10 @@
       val info_graph =
         infos.foldLeft(Graph.string[Info]) {
           case (graph, info) =>
-            if (graph.defined(info.name))
+            if (graph.defined(info.name)) {
               error("Duplicate session " + quote(info.name) + Position.here(info.pos) +
                 Position.here(graph.get_node(info.name).pos))
+            }
             else graph.new_node(info.name, info)
         }
       val build_graph = add_edges(info_graph, "parent", _.parent)
@@ -784,8 +789,9 @@
 
     def check_sessions(names: List[String]): Unit = {
       val bad_sessions = SortedSet(names.filterNot(defined): _*).toList
-      if (bad_sessions.nonEmpty)
+      if (bad_sessions.nonEmpty) {
         error("Undefined session(s): " + commas_quote(bad_sessions))
+      }
     }
 
     def check_sessions(sel: Selection): Unit =