equal
deleted
inserted
replaced
377 case Some(name) => |
377 case Some(name) => |
378 val qualifier = sessions_structure.theory_qualifier(name) |
378 val qualifier = sessions_structure.theory_qualifier(name) |
379 if (proper_session_theories.contains(name)) { |
379 if (proper_session_theories.contains(name)) { |
380 err("Redundant document theory from this session:") |
380 err("Redundant document theory from this session:") |
381 } |
381 } |
382 else if (build_hierarchy.contains(qualifier)) None |
382 else if ( |
383 else if (dependencies.theories.contains(name)) None |
383 !build_hierarchy.contains(qualifier) && |
384 else err("Document theory from other session not imported properly:") |
384 !dependencies.theories.contains(name) |
|
385 ) { |
|
386 err("Document theory from other session not imported properly:") |
|
387 } |
|
388 else None |
385 } |
389 } |
386 }) |
390 }) |
387 val document_theories = |
391 val document_theories = |
388 info.document_theories.map({ case (thy, _) => known_theories(thy).name }) |
392 info.document_theories.map({ case (thy, _) => known_theories(thy).name }) |
389 |
393 |