src/Pure/Thy/sessions.scala
changeset 72297 17507b48b6f5
parent 72296 ba5b37671528
child 72298 4768b1facec2
equal deleted inserted replaced
72296:ba5b37671528 72297:17507b48b6f5
   230             val known_loaded_files = deps_base.known_loaded_files ++ loaded_files
   230             val known_loaded_files = deps_base.known_loaded_files ++ loaded_files
   231 
   231 
   232             val used_theories_session =
   232             val used_theories_session =
   233               dependencies.theories.filter(name => deps_base.theory_qualifier(name) == session_name)
   233               dependencies.theories.filter(name => deps_base.theory_qualifier(name) == session_name)
   234 
   234 
       
   235             val import_errors =
       
   236             {
       
   237               val known_sessions =
       
   238                 sessions_structure.imports_requirements(List(session_name)).toSet
       
   239               for {
       
   240                 name <- dependencies.theories
       
   241                 qualifier = deps_base.theory_qualifier(name)
       
   242                 if !known_sessions(qualifier)
       
   243               } yield "Bad import of theory " + quote(name.toString) +
       
   244                 ": need to include sessions " + quote(qualifier) + " in ROOT"
       
   245             }
       
   246 
   235             val dir_errors =
   247             val dir_errors =
   236             {
   248             {
   237               val ok = info.dirs.map(_.canonical_file).toSet
   249               val ok = info.dirs.map(_.canonical_file).toSet
   238               val bad =
   250               val bad =
   239                 (for {
   251                 (for {
   285                 known_loaded_files = known_loaded_files,
   297                 known_loaded_files = known_loaded_files,
   286                 overall_syntax = overall_syntax,
   298                 overall_syntax = overall_syntax,
   287                 imported_sources = check_sources(imported_files),
   299                 imported_sources = check_sources(imported_files),
   288                 sources = check_sources(session_files),
   300                 sources = check_sources(session_files),
   289                 session_graph_display = session_graph_display,
   301                 session_graph_display = session_graph_display,
   290                 errors = dependencies.errors ::: dir_errors ::: sources_errors :::
   302                 errors = dependencies.errors ::: import_errors ::: dir_errors :::
   291                   path_errors ::: bibtex_errors)
   303                   sources_errors ::: path_errors ::: bibtex_errors)
   292 
   304 
   293             session_bases + (info.name -> base)
   305             session_bases + (info.name -> base)
   294           }
   306           }
   295           catch {
   307           catch {
   296             case ERROR(msg) =>
   308             case ERROR(msg) =>