added official Text.Range.Ordering;
authorwenzelm
Mon Aug 22 16:12:23 2011 +0200 (2011-08-22)
changeset 443791079ab6b342b
parent 44378 81b4af4cfa5a
child 44380 1b1afb1380ee
added official Text.Range.Ordering;
some support for text perspective;
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/text.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Mon Aug 22 14:15:52 2011 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Mon Aug 22 16:12:23 2011 +0200
     1.3 @@ -22,10 +22,7 @@
     1.4      type Entry = (Text.Info[Any], Markup_Tree)
     1.5      type T = SortedMap[Text.Range, Entry]
     1.6  
     1.7 -    val empty = SortedMap.empty[Text.Range, Entry](new scala.math.Ordering[Text.Range]
     1.8 -      {
     1.9 -        def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
    1.10 -      })
    1.11 +    val empty = SortedMap.empty[Text.Range, Entry](Text.Range.Ordering)
    1.12  
    1.13      def update(branches: T, entry: Entry): T = branches + (entry._1.range -> entry)
    1.14      def single(entry: Entry): T = update(empty, entry)
     2.1 --- a/src/Pure/PIDE/text.scala	Mon Aug 22 14:15:52 2011 +0200
     2.2 +++ b/src/Pure/PIDE/text.scala	Mon Aug 22 16:12:23 2011 +0200
     2.3 @@ -8,6 +8,11 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 +import scala.collection.mutable
     2.8 +import scala.math.Ordering
     2.9 +import scala.util.Sorting
    2.10 +
    2.11 +
    2.12  object Text
    2.13  {
    2.14    /* offset */
    2.15 @@ -20,6 +25,11 @@
    2.16    object Range
    2.17    {
    2.18      def apply(start: Offset): Range = Range(start, start)
    2.19 +
    2.20 +    object Ordering extends scala.math.Ordering[Text.Range]
    2.21 +    {
    2.22 +      def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
    2.23 +    }
    2.24    }
    2.25  
    2.26    sealed case class Range(val start: Offset, val stop: Offset)
    2.27 @@ -50,6 +60,33 @@
    2.28    }
    2.29  
    2.30  
    2.31 +  /* perspective */
    2.32 +
    2.33 +  type Perspective = List[Range]  // partitioning in canonical order
    2.34 +
    2.35 +  def perspective(ranges: Seq[Range]): Perspective =
    2.36 +  {
    2.37 +    val sorted_ranges = ranges.toArray
    2.38 +    Sorting.quickSort(sorted_ranges)(Range.Ordering)
    2.39 +
    2.40 +    val result = new mutable.ListBuffer[Text.Range]
    2.41 +    var last: Option[Text.Range] = None
    2.42 +    for (range <- sorted_ranges)
    2.43 +    {
    2.44 +      last match {
    2.45 +        case Some(last_range)
    2.46 +        if ((last_range overlaps range) || last_range.stop == range.start) =>
    2.47 +          last = Some(Text.Range(last_range.start, range.stop))
    2.48 +        case _ =>
    2.49 +          result ++= last
    2.50 +          last = Some(range)
    2.51 +      }
    2.52 +    }
    2.53 +    result ++= last
    2.54 +    result.toList
    2.55 +  }
    2.56 +
    2.57 +
    2.58    /* information associated with text range */
    2.59  
    2.60    sealed case class Info[A](val range: Text.Range, val info: A)
     3.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Aug 22 14:15:52 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Aug 22 16:12:23 2011 +0200
     3.3 @@ -99,6 +99,19 @@
     3.4    }
     3.5  
     3.6  
     3.7 +  /* perspective */
     3.8 +
     3.9 +  def perspective(): Text.Perspective =
    3.10 +  {
    3.11 +    Swing_Thread.require()
    3.12 +    Text.perspective(
    3.13 +      for {
    3.14 +        doc_view <- Isabelle.document_views(buffer)
    3.15 +        range <- doc_view.perspective()
    3.16 +      } yield range)
    3.17 +  }
    3.18 +
    3.19 +
    3.20    /* snapshot */
    3.21  
    3.22    def snapshot(): Document.Snapshot =
     4.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Aug 22 14:15:52 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Aug 22 16:12:23 2011 +0200
     4.3 @@ -10,6 +10,7 @@
     4.4  
     4.5  import isabelle._
     4.6  
     4.7 +import scala.collection.mutable
     4.8  import scala.actors.Actor._
     4.9  
    4.10  import java.lang.System
    4.11 @@ -111,6 +112,22 @@
    4.12    }
    4.13  
    4.14  
    4.15 +  /* perspective */
    4.16 +
    4.17 +  def perspective(): Text.Perspective =
    4.18 +  {
    4.19 +    Swing_Thread.require()
    4.20 +    Text.perspective(
    4.21 +      for {
    4.22 +        i <- 0 until text_area.getVisibleLines
    4.23 +        val start = text_area.getScreenLineStartOffset(i)
    4.24 +        val stop = text_area.getScreenLineEndOffset(i)
    4.25 +        if start >= 0 && stop >= 0
    4.26 +      }
    4.27 +      yield Text.Range(start, stop))
    4.28 +  }
    4.29 +
    4.30 +
    4.31    /* snapshot */
    4.32  
    4.33    // owned by Swing thread
     5.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 22 14:15:52 2011 +0200
     5.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Aug 22 16:12:23 2011 +0200
     5.3 @@ -199,6 +199,13 @@
     5.4    def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
     5.5    def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
     5.6  
     5.7 +  def document_views(buffer: Buffer): List[Document_View] =
     5.8 +    for {
     5.9 +      text_area <- jedit_text_areas(buffer).toList
    5.10 +      val doc_view = document_view(text_area)
    5.11 +      if doc_view.isDefined
    5.12 +    } yield doc_view.get
    5.13 +
    5.14    def init_model(buffer: Buffer)
    5.15    {
    5.16      swing_buffer_lock(buffer) {