src/Pure/Thy/sessions.scala
changeset 70686 9cde8c4ea5a5
parent 70685 c1597167563e
child 70687 086575316fd5
equal deleted inserted replaced
70685:c1597167563e 70686:9cde8c4ea5a5
   180 
   180 
   181     def get_imports: Base =
   181     def get_imports: Base =
   182       imports getOrElse Base.bootstrap(session_directories, global_theories)
   182       imports getOrElse Base.bootstrap(session_directories, global_theories)
   183   }
   183   }
   184 
   184 
   185   sealed case class Deps(
   185   sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base])
   186     sessions_structure: Structure, session_bases: Map[String, Base], all_known: Known)
       
   187   {
   186   {
   188     override def toString: String = "Sessions.Deps(" + sessions_structure + ")"
   187     override def toString: String = "Sessions.Deps(" + sessions_structure + ")"
   189 
   188 
   190     def is_empty: Boolean = session_bases.isEmpty
   189     def is_empty: Boolean = session_bases.isEmpty
   191     def apply(name: String): Base = session_bases(name)
   190     def apply(name: String): Base = session_bases(name)
   427               cat_error(msg, "The error(s) above occurred in session " +
   426               cat_error(msg, "The error(s) above occurred in session " +
   428                 quote(info.name) + Position.here(info.pos))
   427                 quote(info.name) + Position.here(info.pos))
   429           }
   428           }
   430       })
   429       })
   431 
   430 
   432     val all_known =
   431     Deps(sessions_structure, session_bases)
   433       Known.make(Path.current, sessions_structure.imports_topological_order.map(session_bases(_)))
       
   434 
       
   435     Deps(sessions_structure, session_bases, all_known)
       
   436   }
   432   }
   437 
   433 
   438 
   434 
   439   /* base info */
   435   /* base info */
   440 
   436