src/Pure/PIDE/protocol.scala
changeset 46209 aad604f74be0
parent 46207 e76b77356ed6
child 46227 4aa84f84d5e8
equal deleted inserted replaced
46208:4cab63a6dc16 46209:aad604f74be0
    39         case _: XML.XML_Body => None
    39         case _: XML.XML_Body => None
    40       }
    40       }
    41   }
    41   }
    42 
    42 
    43 
    43 
    44   /* toplevel transactions */
    44   /* command status */
    45 
    45 
    46   sealed case class Status(
    46   sealed case class Status(
    47     private val finished: Boolean = false,
    47     private val finished: Boolean = false,
    48     private val failed: Boolean = false,
    48     private val failed: Boolean = false,
    49     forks: Int = 0)
    49     forks: Int = 0)
    67       case _ => status
    67       case _ => status
    68     }
    68     }
    69 
    69 
    70   def command_status(markups: List[Markup]): Status =
    70   def command_status(markups: List[Markup]): Status =
    71     (Status() /: markups)(command_status(_, _))
    71     (Status() /: markups)(command_status(_, _))
       
    72 
       
    73 
       
    74   /* node status */
    72 
    75 
    73   sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
    76   sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
    74   {
    77   {
    75     def total: Int = unprocessed + running + finished + failed
    78     def total: Int = unprocessed + running + finished + failed
    76   }
    79   }