src/Pure/PIDE/protocol.scala
changeset 66379 6392766f3c25
parent 65532 febfd9f78bd4
child 66410 72a7e29104f1
     1.1 --- a/src/Pure/PIDE/protocol.scala	Tue Aug 08 12:21:29 2017 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Aug 08 22:13:05 2017 +0200
     1.3 @@ -352,6 +352,9 @@
     1.4  
     1.5    /* execution */
     1.6  
     1.7 +  def consolidate_execution(): Unit =
     1.8 +    protocol_command("Document.consolidate_execution")
     1.9 +
    1.10    def discontinue_execution(): Unit =
    1.11      protocol_command("Document.discontinue_execution")
    1.12