src/Tools/jEdit/src/document_model.scala

--- a/src/Tools/jEdit/src/document_model.scala	Wed Aug 24 23:20:05 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Aug 25 11:27:37 2011 +0200
@@ -74,10 +74,10 @@
   def perspective(): Text.Perspective =
   {
     Swing_Thread.require()
-    Text.perspective(
+    Text.Perspective(
       for {
         doc_view <- Isabelle.document_views(buffer)
-        range <- doc_view.perspective()
+        range <- doc_view.perspective().ranges
       } yield range)
   }
 
@@ -88,7 +88,7 @@
   {
     private val pending = new mutable.ListBuffer[Text.Edit]
     private var pending_perspective = false
-    private var last_perspective: Text.Perspective = Nil
+    private var last_perspective: Text.Perspective = Text.Perspective.empty
 
     def snapshot(): List[Text.Edit] = pending.toList