114 }) |
114 }) |
115 |
115 |
116 |
116 |
117 /* resolve dependencies */ |
117 /* resolve dependencies */ |
118 |
118 |
|
119 val thy_info = new Thy_Info(this) |
|
120 |
119 def resolve_dependencies(session: Session): Boolean = |
121 def resolve_dependencies(session: Session): Boolean = |
120 { |
122 { |
121 val thys = |
|
122 (for ((_, model) <- state.value.models.iterator if model.is_theory) |
|
123 yield (model.node_name, Position.none)).toList |
|
124 val deps = new Thy_Info(this).dependencies("", thys).deps |
|
125 |
|
126 state.change_result(st => |
123 state.change_result(st => |
127 { |
124 { |
|
125 val thys = |
|
126 (for ((_, model) <- st.models.iterator if model.is_theory) |
|
127 yield (model.node_name, Position.none)).toList |
|
128 |
128 val loaded_models = |
129 val loaded_models = |
129 for { |
130 (for { |
130 uri <- deps.map(_.name.node) |
131 dep <- thy_info.dependencies("", thys).deps.iterator |
131 if get_model(uri).isEmpty |
132 uri = dep.name.node |
|
133 if !st.models.isDefinedAt(uri) |
132 text <- |
134 text <- |
133 try { Some(File.read(Url.file(uri))) } |
135 try { Some(File.read(Url.file(uri))) } |
134 catch { case ERROR(_) => None } |
136 catch { case ERROR(_) => None } |
135 } |
137 } |
136 yield { |
138 yield { |
137 val model = Document_Model.init(session, uri) |
139 val model = Document_Model.init(session, uri) |
138 val model1 = (model.update_text(text) getOrElse model).external(true) |
140 val model1 = (model.update_text(text) getOrElse model).external(true) |
139 (uri, model1) |
141 (uri, model1) |
140 } |
142 }).toList |
|
143 |
141 if (loaded_models.isEmpty) (false, st) |
144 if (loaded_models.isEmpty) (false, st) |
142 else |
145 else |
143 (true, |
146 (true, |
144 st.copy( |
147 st.copy( |
145 models = st.models ++ loaded_models, |
148 models = st.models ++ loaded_models, |
146 pending_input = st.pending_input ++ loaded_models.map(_._1))) |
149 pending_input = st.pending_input ++ loaded_models.iterator.map(_._1))) |
147 }) |
150 }) |
148 } |
151 } |
149 |
152 |
150 |
153 |
151 /* pending input */ |
154 /* pending input */ |