equal
deleted
inserted
replaced
174 |
174 |
175 val session_theories = |
175 val session_theories = |
176 dependencies.theories.filter(name => deps_base.theory_qualifier(name) == session_name) |
176 dependencies.theories.filter(name => deps_base.theory_qualifier(name) == session_name) |
177 |
177 |
178 val theory_files = dependencies.theories.map(_.path) |
178 val theory_files = dependencies.theories.map(_.path) |
179 |
|
180 dependencies.load_commands |
|
181 |
179 |
182 val (load_commands, load_commands_errors) = |
180 val (load_commands, load_commands_errors) = |
183 try { if (inlined_files) (dependencies.load_commands, Nil) else (Nil, Nil) } |
181 try { if (inlined_files) (dependencies.load_commands, Nil) else (Nil, Nil) } |
184 catch { case ERROR(msg) => (Nil, List(msg)) } |
182 catch { case ERROR(msg) => (Nil, List(msg)) } |
185 |
183 |