do not store bulky Session.Deps;
authorwenzelm
Wed, 01 Nov 2017 16:38:15 +0100
changeset 66975 ca73d44d51aa
parent 66974 b14c24b31f45
child 66976 806bc39550a5
do not store bulky Session.Deps;
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)
   }