# HG changeset patch
# User wenzelm
# Date 1678189210 -3600
# Node ID 5749ee7c45a056ec4062a69e5f3aec62313973b0
# Parent  4ad322ee6025f380baf8d672f5a74cdcbab40e8f
clarified signature: proper abstract type;

diff -r 4ad322ee6025 -r 5749ee7c45a0 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Mar 07 12:21:45 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Mar 07 12:40:10 2023 +0100
@@ -269,7 +269,10 @@
 
   /* source dependencies */
 
-  sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) {
+  final class Deps private[Sessions](
+    val sessions_structure: Structure,
+    val session_bases: Map[String, Base]
+  ) {
     def background(session: String): Background =
       Background(base = apply(session), sessions_structure = sessions_structure, errors = errors)
 
@@ -542,7 +545,7 @@
           }
       }
 
-    Deps(sessions_structure, session_bases)
+    new Deps(sessions_structure, session_bases)
   }