equal
deleted
inserted
replaced
89 case errs => error(cat_lines(errs)) |
89 case errs => error(cat_lines(errs)) |
90 } |
90 } |
91 } |
91 } |
92 |
92 |
93 val known_theories = |
93 val known_theories = |
94 (parent_base.known_theories /: thy_deps.deps)({ case (known, dep) => |
94 { |
95 val name = dep.name |
95 val imports_iterator = |
96 known.get(name.theory) match { |
96 for { |
97 case Some(name1) if name != name1 => |
97 import_session <- info.imports.iterator |
98 error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node)) |
98 (_, name) <- sessions(import_session).known_theories.iterator |
99 case _ => |
99 } yield name |
100 known + (name.theory -> name) + |
100 val deps_iterator = thy_deps.deps.iterator.map(_.name) |
101 (Long_Name.base_name(name.theory) -> name) // legacy |
101 |
102 } |
102 (parent_base.known_theories /: (imports_iterator ++ deps_iterator))({ |
103 }) |
103 case (known, name) => |
|
104 known.get(name.theory) match { |
|
105 case Some(name1) if name != name1 => |
|
106 error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node)) |
|
107 case _ => |
|
108 known + (name.theory -> name) + |
|
109 (Long_Name.base_name(name.theory) -> name) // legacy |
|
110 } |
|
111 }) |
|
112 } |
104 |
113 |
105 val loaded_theories = thy_deps.loaded_theories |
114 val loaded_theories = thy_deps.loaded_theories |
106 val keywords = thy_deps.keywords |
115 val keywords = thy_deps.keywords |
107 val syntax = thy_deps.syntax |
116 val syntax = thy_deps.syntax |
108 |
117 |