src/Pure/PIDE/document_status.scala
changeset 70025 b21ddfa7042b
parent 69998 60d0ee8f2ddb
child 70044 9532d5b2e932
equal deleted inserted replaced
70024:edda2d14c108 70025:b21ddfa7042b
   162     consolidated: Boolean)
   162     consolidated: Boolean)
   163   {
   163   {
   164     def ok: Boolean = failed == 0
   164     def ok: Boolean = failed == 0
   165     def total: Int = unprocessed + running + warned + failed + finished
   165     def total: Int = unprocessed + running + warned + failed + finished
   166 
   166 
   167     def quasi_consolidated: Boolean = !finalized && terminated
   167     def quasi_consolidated: Boolean = !is_suppressed && !finalized && terminated
   168 
   168 
   169     def percentage: Int =
   169     def percentage: Int =
   170       if (consolidated) 100
   170       if (consolidated) 100
   171       else if (total == 0) 0
   171       else if (total == 0) 0
   172       else (((total - unprocessed).toDouble / total) * 100).toInt min 99
   172       else (((total - unprocessed).toDouble / total) * 100).toInt min 99