src/Pure/Thy/sessions.scala
changeset 76868 2329e106cfcd
parent 76867 165ba28378f6
child 76869 9ed58e165110
--- a/src/Pure/Thy/sessions.scala	Mon Jan 02 15:18:13 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Jan 02 15:28:33 2023 +0100
@@ -1661,18 +1661,22 @@
       }
     }
 
-    def read_sources(db: SQL.Database, session_name: String, name: String): Option[Source_File] = {
-      val sql =
-        Sources.table.select(Nil, Sources.where_equal(session_name, name = name))
-      db.using_statement(sql) { stmt =>
-        val res = stmt.execute_query()
-        if (!res.next()) None
-        else {
+    def read_sources(
+      db: SQL.Database,
+      session_name: String,
+      name: String = ""
+    ): List[Source_File] = {
+      val select =
+        Sources.table.select(Nil,
+          Sources.where_equal(session_name, name = name) + " ORDER BY " + Sources.name)
+      db.using_statement(select) { stmt =>
+        (stmt.execute_query().iterator { res =>
+          val res_name = res.string(Sources.name)
           val digest = SHA1.fake_digest(res.string(Sources.digest))
           val compressed = res.bool(Sources.compressed)
           val body = res.bytes(Sources.body)
-          Some(Source_File(name, digest, compressed, body, cache.compress))
-        }
+          Source_File(res_name, digest, compressed, body, cache.compress)
+        }).toList
       }
     }
   }