src/Pure/PIDE/command.scala
changeset 44385 e7fdb008aa7d
parent 44384 8f6054a63f96
child 44474 681447a9ffe5
     1.1 --- a/src/Pure/PIDE/command.scala	Mon Aug 22 21:42:02 2011 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Aug 23 12:20:12 2011 +0200
     1.3 @@ -89,6 +89,14 @@
     1.4    /* perspective */
     1.5  
     1.6    type Perspective = List[Command]  // visible commands in canonical order
     1.7 +
     1.8 +  def equal_perspective(p1: Perspective, p2: Perspective): Boolean =
     1.9 +  {
    1.10 +    require(p1.forall(_.is_defined))
    1.11 +    require(p2.forall(_.is_defined))
    1.12 +    p1.length == p2.length &&
    1.13 +      (p1.iterator zip p2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
    1.14 +  }
    1.15  }
    1.16  
    1.17  
    1.18 @@ -98,12 +106,12 @@
    1.19  {
    1.20    /* classification */
    1.21  
    1.22 +  def is_defined: Boolean = id != Document.no_id
    1.23 +
    1.24    def is_command: Boolean = !span.isEmpty && span.head.is_command
    1.25    def is_ignored: Boolean = span.forall(_.is_ignored)
    1.26    def is_malformed: Boolean = !is_command && !is_ignored
    1.27  
    1.28 -  def is_unparsed = id == Document.no_id
    1.29 -
    1.30    def name: String = if (is_command) span.head.content else ""
    1.31    override def toString =
    1.32      id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")