--- a/src/Pure/PIDE/protocol.scala Mon Oct 16 14:21:14 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala Mon Oct 16 14:32:09 2017 +0200
@@ -113,7 +113,7 @@
{
def unapply(props: Properties.T): Option[(Document_ID.Generic, isabelle.Timing)] =
props match {
- case (Markup.FUNCTION, Markup.COMMAND_TIMING) :: args =>
+ case Markup.COMMAND_TIMING :: args =>
(args, args) match {
case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing))
case _ => None
@@ -123,6 +123,22 @@
}
+ /* theory timing */
+
+ object Theory_Timing
+ {
+ def unapply(props: Properties.T): Option[(String, isabelle.Timing)] =
+ props match {
+ case Markup.THEORY_TIMING :: args =>
+ (args, args) match {
+ case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing))
+ case _ => None
+ }
+ case _ => None
+ }
+ }
+
+
/* node status */
sealed case class Node_Status(