88 |
88 |
89 |
89 |
90 /* theories */ |
90 /* theories */ |
91 |
91 |
92 def use_theories( |
92 def use_theories( |
93 theories: List[(String, Position.T)], |
93 theories: List[String], |
94 qualifier: String = Sessions.DRAFT, |
94 qualifier: String = Sessions.DRAFT, |
95 master_dir: String = "", |
95 master_dir: String = "", |
96 id: UUID = UUID(), |
96 id: UUID = UUID(), |
97 progress: Progress = No_Progress): Theories_Result = |
97 progress: Progress = No_Progress): Theories_Result = |
98 { |
98 { |
229 private val state = Synchronized(Thy_Resources.State()) |
229 private val state = Synchronized(Thy_Resources.State()) |
230 |
230 |
231 def load_theories( |
231 def load_theories( |
232 session: Session, |
232 session: Session, |
233 id: UUID, |
233 id: UUID, |
234 theories: List[(String, Position.T)], |
234 theories: List[String], |
235 qualifier: String = Sessions.DRAFT, |
235 qualifier: String = Sessions.DRAFT, |
236 master_dir: String = "", |
236 master_dir: String = "", |
237 progress: Progress = No_Progress): List[Document.Node.Name] = |
237 progress: Progress = No_Progress): List[Document.Node.Name] = |
238 { |
238 { |
239 val import_names = |
239 val import_names = theories.map(thy => import_name(qualifier, master_dir, thy) -> Position.none) |
240 for ((thy, pos) <- theories) |
|
241 yield (import_name(qualifier, master_dir, thy), pos) |
|
242 |
|
243 val dependencies = resources.dependencies(import_names, progress = progress).check_errors |
240 val dependencies = resources.dependencies(import_names, progress = progress).check_errors |
244 val dep_theories = dependencies.theories |
241 val dep_theories = dependencies.theories |
245 |
242 |
246 val loaded_theories = |
243 val loaded_theories = |
247 for (node_name <- dep_theories) |
244 for (node_name <- dep_theories) |