src/Pure/PIDE/session.scala
changeset 66873 9953ae603a23
parent 66720 b07192253605
child 67825 f9c071cc958b
     1.1 --- a/src/Pure/PIDE/session.scala	Mon Oct 16 14:21:14 2017 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Mon Oct 16 14:32:09 2017 +0200
     1.3 @@ -432,6 +432,9 @@
     1.4                  val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
     1.5                  accumulate(state_id, xml_cache.elem(message))
     1.6  
     1.7 +              case Protocol.Theory_Timing(_, _) =>
     1.8 +                // FIXME
     1.9 +
    1.10                case Markup.Assign_Update =>
    1.11                  msg.text match {
    1.12                    case Protocol.Assign_Update(id, update) =>