# HG changeset patch
# User wenzelm
# Date 1509550695 -3600
# Node ID ca73d44d51aaeae2458d96601de9cbfd54dbe094
# Parent  b14c24b31f456cf79b6b110120e71e9dd074c777
do not store bulky Session.Deps;

diff -r b14c24b31f45 -r ca73d44d51aa src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Nov 01 16:31:27 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Nov 01 16:38:15 2017 +0100
@@ -328,11 +328,10 @@
   sealed case class Base_Info(
     session: String,
     sessions: T,
-    deps: Deps,
+    errors: List[String],
     base: Base,
     infos: List[Info])
   {
-    def errors: List[String] = deps.errors
     def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
   }
 
@@ -396,7 +395,7 @@
     val deps1 = Sessions.deps(sessions1, global_theories)
     val base1 = if (all_known) deps1(session1).copy(known = deps1.all_known) else deps1(session1)
 
-    Base_Info(session1, sessions1, deps1, base1, infos1)
+    Base_Info(session1, sessions1, deps1.errors, base1, infos1)
   }