slightly more abstract Command.Perspective;

--- 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 })
+    }
   }
 }
 

--- a/src/Pure/PIDE/document.scala	Thu Aug 25 11:27:37 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Aug 25 11:41:48 2011 +0200
@@ -60,7 +60,8 @@
         case exn => exn
       }
 
-    val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Nil, Map(), Linear_Set())
+    val empty: Node =
+      Node(Exn.Exn(ERROR("Bad theory header")), Command.Perspective.empty, Map(), Linear_Set())
 
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
       : Iterator[(Command, Text.Offset)] =

--- a/src/Pure/PIDE/isar_document.scala	Thu Aug 25 11:27:37 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Thu Aug 25 11:41:48 2011 +0200
@@ -144,7 +144,7 @@
   {
     val ids =
     { import XML.Encode._
-      list(long)(perspective.map(_.id)) }
+      list(long)(perspective.commands.map(_.id)) }
 
     input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id), name,
       YXML.string_of_body(ids))
@@ -164,7 +164,7 @@
             { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
                 (Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) },
             { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
-            { case Document.Node.Perspective(cs) => (cs.map(c => long_atom(c.id)), Nil) }))))
+            { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))))
       YXML.string_of_body(encode(edits)) }
 
     input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)

--- a/src/Pure/PIDE/text.scala	Thu Aug 25 11:27:37 2011 +0200
+++ b/src/Pure/PIDE/text.scala	Thu Aug 25 11:41:48 2011 +0200
@@ -64,7 +64,7 @@
 
   object Perspective
   {
-    val empty = Perspective(Nil)
+    val empty: Perspective = Perspective(Nil)
 
     def apply(ranges: Seq[Range]): Perspective =
     {

--- a/src/Pure/Thy/thy_syntax.scala	Thu Aug 25 11:27:37 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Aug 25 11:41:48 2011 +0200
@@ -101,7 +101,7 @@
 
   def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
   {
-    if (perspective.is_empty) Nil
+    if (perspective.is_empty) Command.Perspective.empty
     else {
       val result = new mutable.ListBuffer[Command]
       @tailrec
@@ -121,7 +121,7 @@
         }
       }
       check_ranges(perspective.ranges, node.command_range(perspective.range).toStream)
-      result.toList
+      Command.Perspective(result.toList)
     }
   }
 
@@ -131,7 +131,7 @@
     val node = nodes(name)
     val perspective = command_perspective(node, text_perspective)
     val new_nodes =
-      if (Command.equal_perspective(node.perspective, perspective)) None
+      if (node.perspective same perspective) None
       else Some(nodes + (name -> node.copy(perspective = perspective)))
     (perspective, new_nodes)
   }