equal
deleted
inserted
replaced
111 private def delay_load_body(): Unit = { |
111 private def delay_load_body(): Unit = { |
112 val required_files = { |
112 val required_files = { |
113 val models = Document_Model.get_models() |
113 val models = Document_Model.get_models() |
114 |
114 |
115 val thy_files = |
115 val thy_files = |
116 resources.resolve_dependencies(models.values, |
116 resources.resolve_dependencies(models.values, PIDE.editor.document_required()) |
117 PIDE.editor.document_required().map((_, Position.none))) |
|
118 |
117 |
119 val aux_files = |
118 val aux_files = |
120 if (resources.auto_resolve) { |
119 if (resources.auto_resolve) { |
121 session.stable_tip_version(models.values) match { |
120 session.stable_tip_version(models.values) match { |
122 case Some(version) => resources.undefined_blobs(version) |
121 case Some(version) => resources.undefined_blobs(version) |