--- a/src/Pure/PIDE/isar_document.scala Fri Aug 20 11:47:33 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala Fri Aug 20 11:57:43 2010 +0200
@@ -1,7 +1,7 @@
/* Title: Pure/PIDE/isar_document.scala
Author: Makarius
-Protocol commands for interactive Isar documents.
+Protocol message formats for interactive Isar documents.
*/
package isabelle
@@ -9,7 +9,7 @@
object Isar_Document
{
- /* protocol messages */
+ /* document editing */
object Assign {
def unapply(msg: XML.Tree)
@@ -32,6 +32,30 @@
case _ => None
}
}
+
+
+ /* toplevel transactions */
+
+ sealed abstract class Status
+ case class Forked(forks: Int) extends Status
+ case object Unprocessed extends Status
+ case object Finished extends Status
+ case object Failed extends Status
+
+ def command_status(markup: XML.Body): Status =
+ {
+ val forks = (0 /: markup) {
+ case (i, XML.Elem(Markup(Markup.FORKED, _), _)) => i + 1
+ case (i, XML.Elem(Markup(Markup.JOINED, _), _)) => i - 1
+ case (i, _) => i
+ }
+ if (forks != 0) Forked(forks)
+ else if (markup.exists { case XML.Elem(Markup(Markup.FAILED, _), _) => true case _ => false })
+ Failed
+ else if (markup.exists { case XML.Elem(Markup(Markup.FINISHED, _), _) => true case _ => false })
+ Finished
+ else Unprocessed
+ }
}