equal
deleted
inserted
replaced
251 (for ((_, model) <- st.buffer_models.iterator) yield model.node_name).toList |
251 (for ((_, model) <- st.buffer_models.iterator) yield model.node_name).toList |
252 val touched_nodes = model_edits.map(_._1) |
252 val touched_nodes = model_edits.map(_._1) |
253 val pending_nodes = for ((node_name, None) <- purged) yield node_name |
253 val pending_nodes = for ((node_name, None) <- purged) yield node_name |
254 (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none)) |
254 (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none)) |
255 } |
255 } |
256 val retain = PIDE.resources.dependencies(imports).names.toSet |
256 val retain = PIDE.resources.dependencies(imports).theories.toSet |
257 |
257 |
258 for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits) |
258 for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits) |
259 yield edit |
259 yield edit |
260 } |
260 } |
261 else Nil |
261 else Nil |