src/Tools/jEdit/src/document_model.scala
changeset 67059 df7d728103f1
parent 67014 e6a695d6a6b2
child 67244 318f44a5c164
equal deleted inserted replaced
67058:03d4954c68bb 67059:df7d728103f1
   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