src/Pure/PIDE/protocol.scala
changeset 56743 81370dfadb1d
parent 56616 abc2da18d08d
child 56746 d37a5d09a277
     1.1 --- a/src/Pure/PIDE/protocol.scala	Sat Apr 26 06:43:06 2014 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Apr 26 13:07:20 2014 +0200
     1.3 @@ -101,7 +101,7 @@
     1.4    }
     1.5  
     1.6    val proper_status_elements =
     1.7 -    Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
     1.8 +    Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
     1.9        Markup.FINISHED, Markup.FAILED)
    1.10  
    1.11    val liberal_status_elements =
    1.12 @@ -187,7 +187,7 @@
    1.13    /* result messages */
    1.14  
    1.15    private val clean_elements =
    1.16 -    Document.Elements(Markup.REPORT, Markup.NO_REPORT)
    1.17 +    Markup.Elements(Markup.REPORT, Markup.NO_REPORT)
    1.18  
    1.19    def clean_message(body: XML.Body): XML.Body =
    1.20      body filter {
    1.21 @@ -308,7 +308,7 @@
    1.22    /* reported positions */
    1.23  
    1.24    private val position_elements =
    1.25 -    Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    1.26 +    Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    1.27  
    1.28    def message_positions(
    1.29      self_id: Document_ID.Generic => Boolean,