src/Tools/jEdit/src/document_view.scala
changeset 44379 1079ab6b342b
parent 44378 81b4af4cfa5a
child 44436 546adfa8a6fc
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Aug 22 14:15:52 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Aug 22 16:12:23 2011 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 +import scala.collection.mutable
     1.8  import scala.actors.Actor._
     1.9  
    1.10  import java.lang.System
    1.11 @@ -111,6 +112,22 @@
    1.12    }
    1.13  
    1.14  
    1.15 +  /* perspective */
    1.16 +
    1.17 +  def perspective(): Text.Perspective =
    1.18 +  {
    1.19 +    Swing_Thread.require()
    1.20 +    Text.perspective(
    1.21 +      for {
    1.22 +        i <- 0 until text_area.getVisibleLines
    1.23 +        val start = text_area.getScreenLineStartOffset(i)
    1.24 +        val stop = text_area.getScreenLineEndOffset(i)
    1.25 +        if start >= 0 && stop >= 0
    1.26 +      }
    1.27 +      yield Text.Range(start, stop))
    1.28 +  }
    1.29 +
    1.30 +
    1.31    /* snapshot */
    1.32  
    1.33    // owned by Swing thread