src/Tools/jEdit/src/document_model.scala

--- a/src/Tools/jEdit/src/document_model.scala	Mon Aug 22 14:15:52 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Aug 22 16:12:23 2011 +0200
@@ -99,6 +99,19 @@
   }
 
 
+  /* perspective */
+
+  def perspective(): Text.Perspective =
+  {
+    Swing_Thread.require()
+    Text.perspective(
+      for {
+        doc_view <- Isabelle.document_views(buffer)
+        range <- doc_view.perspective()
+      } yield range)
+  }
+
+
   /* snapshot */
 
   def snapshot(): Document.Snapshot =