equal
deleted
inserted
replaced
228 { |
228 { |
229 def is_empty: Boolean = rep.isEmpty |
229 def is_empty: Boolean = rep.isEmpty |
230 def apply(name: Document.Node.Name): Node_Status = rep(name) |
230 def apply(name: Document.Node.Name): Node_Status = rep(name) |
231 def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name) |
231 def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name) |
232 |
232 |
233 def present: List[(Document.Node.Name, Node_Status)] = |
233 def present(snapshot: Document.Snapshot): List[(Document.Node.Name, Node_Status)] = |
234 for { name <- nodes.topological_order; node_status <- get(name) } |
234 (for { |
235 yield (name, node_status) |
235 name <- nodes.topological_order.iterator |
|
236 node_status <- get(name) |
|
237 if !snapshot.version.nodes.is_suppressed(name) |
|
238 } yield (name, node_status)).toList |
236 |
239 |
237 def quasi_consolidated(name: Document.Node.Name): Boolean = |
240 def quasi_consolidated(name: Document.Node.Name): Boolean = |
238 rep.get(name) match { |
241 rep.get(name) match { |
239 case Some(st) => st.quasi_consolidated |
242 case Some(st) => st.quasi_consolidated |
240 case None => false |
243 case None => false |
256 { |
259 { |
257 val nodes1 = version.nodes |
260 val nodes1 = version.nodes |
258 val update_iterator = |
261 val update_iterator = |
259 for { |
262 for { |
260 name <- domain.getOrElse(nodes1.domain).iterator |
263 name <- domain.getOrElse(nodes1.domain).iterator |
261 if !resources.is_hidden(name) && |
264 if !resources.is_hidden(name) && !resources.session_base.loaded_theory(name) |
262 !resources.session_base.loaded_theory(name) && |
|
263 !nodes1.is_suppressed(name) && |
|
264 !nodes1(name).is_empty |
|
265 st = Document_Status.Node_Status.make(state, version, name) |
265 st = Document_Status.Node_Status.make(state, version, name) |
266 if !rep.isDefinedAt(name) || rep(name) != st |
266 if !rep.isDefinedAt(name) || rep(name) != st |
267 } yield (name -> st) |
267 } yield (name -> st) |
268 val rep1 = rep ++ update_iterator |
268 val rep1 = rep ++ update_iterator |
269 val rep2 = if (trim) rep1 -- rep1.keysIterator.filterNot(nodes1.domain) else rep1 |
269 val rep2 = if (trim) rep1 -- rep1.keysIterator.filterNot(nodes1.domain) else rep1 |