equal
deleted
inserted
replaced
190 case Some(names) => names.iterator.map(name => (name, nodes(name))) |
190 case Some(names) => names.iterator.map(name => (name, nodes(name))) |
191 case None => nodes.iterator |
191 case None => nodes.iterator |
192 } |
192 } |
193 val nodes_status1 = |
193 val nodes_status1 = |
194 (nodes_status /: iterator)({ case (status, (name, node)) => |
194 (nodes_status /: iterator)({ case (status, (name, node)) => |
195 if (!name.is_theory || PIDE.resources.base.loaded_theory(name) || node.is_empty) |
195 if (!name.is_theory || PIDE.resources.session_base.loaded_theory(name) || node.is_empty) |
196 status |
196 status |
197 else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) }) |
197 else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) }) |
198 |
198 |
199 val nodes_status2 = |
199 val nodes_status2 = |
200 nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_hidden(_)) |
200 nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_hidden(_)) |