src/Pure/PIDE/document_status.scala
changeset 70658 4655897b8287
parent 70653 f7c5b30fc432
child 71601 97ccf48c2f0c
equal deleted inserted replaced
70657:2bf1d0e57695 70658:4655897b8287
   242       (for {
   242       (for {
   243         name <- nodes.topological_order.iterator
   243         name <- nodes.topological_order.iterator
   244         node_status <- get(name)
   244         node_status <- get(name)
   245       } yield (name, node_status)).toList
   245       } yield (name, node_status)).toList
   246 
   246 
   247     def consolidated(name: Document.Node.Name): Boolean =
       
   248       rep.get(name) match {
       
   249         case Some(st) => st.consolidated
       
   250         case None => false
       
   251       }
       
   252 
       
   253     def quasi_consolidated(name: Document.Node.Name): Boolean =
   247     def quasi_consolidated(name: Document.Node.Name): Boolean =
   254       rep.get(name) match {
   248       rep.get(name) match {
   255         case Some(st) => st.quasi_consolidated
   249         case Some(st) => st.quasi_consolidated
   256         case None => false
   250         case None => false
   257       }
   251       }