--- a/src/Pure/PIDE/command.scala Thu Aug 25 11:27:37 2011 +0200
+++ b/src/Pure/PIDE/command.scala Thu Aug 25 11:41:48 2011 +0200
@@ -88,14 +88,22 @@
/* perspective */
- type Perspective = List[Command] // visible commands in canonical order
+ object Perspective
+ {
+ val empty: Perspective = Perspective(Nil)
+ }
- def equal_perspective(p1: Perspective, p2: Perspective): Boolean =
+ sealed case class Perspective(commands: List[Command]) // visible commands in canonical order
{
- require(p1.forall(_.is_defined))
- require(p2.forall(_.is_defined))
- p1.length == p2.length &&
- (p1.iterator zip p2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
+ def same(that: Perspective): Boolean =
+ {
+ val cmds1 = this.commands
+ val cmds2 = that.commands
+ require(cmds1.forall(_.is_defined))
+ require(cmds2.forall(_.is_defined))
+ cmds1.length == cmds2.length &&
+ (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
+ }
}
}