src/Pure/PIDE/isar_document.scala
changeset 38567 b670faa807c9
parent 38483 3d16bebee1d3
child 38581 d503a0912e14
     1.1 --- a/src/Pure/PIDE/isar_document.scala	Fri Aug 20 11:47:33 2010 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Fri Aug 20 11:57:43 2010 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  /*  Title:      Pure/PIDE/isar_document.scala
     1.5      Author:     Makarius
     1.6  
     1.7 -Protocol commands for interactive Isar documents.
     1.8 +Protocol message formats for interactive Isar documents.
     1.9  */
    1.10  
    1.11  package isabelle
    1.12 @@ -9,7 +9,7 @@
    1.13  
    1.14  object Isar_Document
    1.15  {
    1.16 -  /* protocol messages */
    1.17 +  /* document editing */
    1.18  
    1.19    object Assign {
    1.20      def unapply(msg: XML.Tree)
    1.21 @@ -32,6 +32,30 @@
    1.22          case _ => None
    1.23        }
    1.24    }
    1.25 +
    1.26 +
    1.27 +  /* toplevel transactions */
    1.28 +
    1.29 +  sealed abstract class Status
    1.30 +  case class Forked(forks: Int) extends Status
    1.31 +  case object Unprocessed extends Status
    1.32 +  case object Finished extends Status
    1.33 +  case object Failed extends Status
    1.34 +
    1.35 +  def command_status(markup: XML.Body): Status =
    1.36 +  {
    1.37 +    val forks = (0 /: markup) {
    1.38 +      case (i, XML.Elem(Markup(Markup.FORKED, _), _)) => i + 1
    1.39 +      case (i, XML.Elem(Markup(Markup.JOINED, _), _)) => i - 1
    1.40 +      case (i, _) => i
    1.41 +    }
    1.42 +    if (forks != 0) Forked(forks)
    1.43 +    else if (markup.exists { case XML.Elem(Markup(Markup.FAILED, _), _) => true case _ => false })
    1.44 +      Failed
    1.45 +    else if (markup.exists { case XML.Elem(Markup(Markup.FINISHED, _), _) => true case _ => false })
    1.46 +      Finished
    1.47 +    else Unprocessed
    1.48 +  }
    1.49  }
    1.50  
    1.51