<commit_before>/*  Title:      Pure/PIDE/protocol.scala
    Author:     Makarius

Protocol message formats for interactive proof documents.
*/

package isabelle


object Protocol
{
  /* document editing */

  object Assign
  {
    def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
      try {
        import XML.Decode._
        val body = YXML.parse_body(text)
        Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body))
      }
      catch {
        case ERROR(_) => None
        case _: XML.XML_Atom => None
        case _: XML.XML_Body => None
      }
  }

  object Removed
  {
    def unapply(text: String): Option[List[Document.Version_ID]] =
      try {
        import XML.Decode._
        Some(list(long)(YXML.parse_body(text)))
      }
      catch {
        case ERROR(_) => None
        case _: XML.XML_Atom => None
        case _: XML.XML_Body => None
      }
  }


  /* toplevel transactions */

  sealed case class Status(
    private val finished: Boolean = false,
    private val failed: Boolean = false,
    forks: Int = 0)
  {
    def is_unprocessed: Boolean = !finished && !failed && forks == 0
    def is_running: Boolean = forks != 0
    def is_finished: Boolean = finished && forks == 0
    def is_failed: Boolean = failed && forks == 0
  }

  val command_status_markup: Set[String] =
    Set(Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
      Isabelle_Markup.FORKED, Isabelle_Markup.JOINED)

  def command_status(status: Status, markup: Markup): Status =
    markup match {
      case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true)
      case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true)
      case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1)
      case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1)
      case _ => status
    }

  def command_status(markups: List[Markup]): Status =
    (Status() /: markups)(command_status(_, _))

  sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
  {
    def total: Int = unprocessed + running + finished + failed
  }

  def node_status(
    state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
  {
    var unprocessed = 0
    var running = 0
    var finished = 0
    var failed = 0
    node.commands.foreach(command =>
      {
        val status = command_status(state.command_state(version, command).status)
        if (status.is_running) running += 1
        else if (status.is_finished) finished += 1
        else if (status.is_failed) failed += 1
        else unprocessed += 1<commit_msg>tuned comments;<commit_after>/*  Title:      Pure/PIDE/protocol.scala
    Author:     Makarius

Protocol message formats for interactive proof documents.
*/

package isabelle


object Protocol
{
  /* document editing */

  object Assign
  {
    def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
      try {
        import XML.Decode._
        val body = YXML.parse_body(text)
        Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body))
      }
      catch {
        case ERROR(_) => None
        case _: XML.XML_Atom => None
        case _: XML.XML_Body => None
      }
  }

  object Removed
  {
    def unapply(text: String): Option[List[Document.Version_ID]] =
      try {
        import XML.Decode._
        Some(list(long)(YXML.parse_body(text)))
      }
      catch {
        case ERROR(_) => None
        case _: XML.XML_Atom => None
        case _: XML.XML_Body => None
      }
  }


  /* command status */

  sealed case class Status(
    private val finished: Boolean = false,
    private val failed: Boolean = false,
    forks: Int = 0)
  {
    def is_unprocessed: Boolean = !finished && !failed && forks == 0
    def is_running: Boolean = forks != 0
    def is_finished: Boolean = finished && forks == 0
    def is_failed: Boolean = failed && forks == 0
  }

  val command_status_markup: Set[String] =
    Set(Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
      Isabelle_Markup.FORKED, Isabelle_Markup.JOINED)

  def command_status(status: Status, markup: Markup): Status =
    markup match {
      case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true)
      case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true)
      case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1)
      case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1)
      case _ => status
    }

  def command_status(markups: List[Markup]): Status =
    (Status() /: markups)(command_status(_, _))


  /* node status */

  sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
  {
    def total: Int = unprocessed + running + finished + failed
  }

  def node_status(
    state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
  {
    var unprocessed = 0
    var running = 0
    var finished = 0
    var failed = 0
    node.commands.foreach(command =>
      {
        val status = command_status(state.command_state(version, command).status)
        if (status.is_running) running += 1
        else if (status.is_finished) finished += 1
        else if (status.is_failed) failed += 1
        else unprocessed += 1
{'fraction_non_alphanumeric': 0.11500830718109654, 'fraction_numerical': 0.005538120731031937, 'mean_word_length': 2.767732962447844, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 27, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1656903', 'n_tokens_mistral': 1783, 'n_tokens_neox': 1710, 'n_words': 424}