src/Tools/jEdit/src/fold_handling.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64621 7116f2634e32
child 66176 b51a40281016
permissions -rw-r--r--
tuned signature;
wenzelm@51240
     1
/*  Title:      Tools/jEdit/src/fold_handling.scala
wenzelm@50542
     2
    Author:     Makarius
wenzelm@50542
     3
wenzelm@50542
     4
Handling of folds within the text structure.
wenzelm@50542
     5
*/
wenzelm@50542
     6
wenzelm@50542
     7
package isabelle.jedit
wenzelm@50542
     8
wenzelm@50542
     9
wenzelm@50542
    10
import isabelle._
wenzelm@50542
    11
wenzelm@58700
    12
import javax.swing.text.Segment
wenzelm@50542
    13
wenzelm@58700
    14
import scala.collection.convert.WrapAsJava
wenzelm@58700
    15
wenzelm@58700
    16
import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler}
wenzelm@50542
    17
wenzelm@50542
    18
wenzelm@50542
    19
object Fold_Handling
wenzelm@50542
    20
{
wenzelm@58694
    21
  /* input: dynamic line context  */
wenzelm@58694
    22
wenzelm@58694
    23
  class Fold_Handler extends FoldHandler("isabelle")
wenzelm@58694
    24
  {
wenzelm@58694
    25
    override def equals(other: Any): Boolean =
wenzelm@58694
    26
      other match {
wenzelm@58694
    27
        case that: Fold_Handler => true
wenzelm@58694
    28
        case _ => false
wenzelm@58694
    29
      }
wenzelm@58694
    30
wenzelm@58694
    31
    override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
wenzelm@63454
    32
      Token_Markup.Line_Context.next(buffer, line).structure.depth max 0
wenzelm@58700
    33
wenzelm@58700
    34
    override def getPrecedingFoldLevels(
wenzelm@58700
    35
      buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] =
wenzelm@58700
    36
    {
wenzelm@63457
    37
      val structure = Token_Markup.Line_Context.next(buffer, line).structure
wenzelm@58700
    38
      val result =
wenzelm@63457
    39
        if (line > 0 && structure.command)
wenzelm@58700
    40
          Range.inclusive(line - 1, 0, -1).iterator.
wenzelm@63454
    41
            map(i => Token_Markup.Line_Context.next(buffer, i).structure).
wenzelm@63457
    42
            takeWhile(_.improper).map(_ => structure.depth max 0).toList
wenzelm@58700
    43
        else Nil
wenzelm@58700
    44
wenzelm@58700
    45
      if (result.isEmpty) null
wenzelm@58700
    46
      else WrapAsJava.seqAsJavaList(result.map(i => new Integer(i)))
wenzelm@58700
    47
    }
wenzelm@58694
    48
  }
wenzelm@58694
    49
wenzelm@58694
    50
wenzelm@58694
    51
  /* output: static document rendering */
wenzelm@58694
    52
wenzelm@64621
    53
  class Document_Fold_Handler(private val rendering: JEdit_Rendering)
wenzelm@50542
    54
    extends FoldHandler("isabelle-document")
wenzelm@50542
    55
  {
wenzelm@50542
    56
    override def equals(other: Any): Boolean =
wenzelm@50542
    57
      other match {
wenzelm@50542
    58
        case that: Document_Fold_Handler => this.rendering == that.rendering
wenzelm@50542
    59
        case _ => false
wenzelm@50542
    60
      }
wenzelm@50542
    61
wenzelm@50542
    62
    override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
wenzelm@50542
    63
    {
wenzelm@50542
    64
      def depth(i: Text.Offset): Int =
wenzelm@50542
    65
        if (i < 0) 0
wenzelm@50542
    66
        else {
wenzelm@58692
    67
          rendering.fold_depth(Text.Range(i, i + 1)) match {
wenzelm@58692
    68
            case Text.Info(_, d) :: _ => d
wenzelm@50542
    69
            case _ => 0
wenzelm@50542
    70
          }
wenzelm@50542
    71
        }
wenzelm@50542
    72
wenzelm@50542
    73
      if (line <= 0) 0
wenzelm@50542
    74
      else {
wenzelm@56589
    75
        val range = JEdit_Lib.line_range(buffer, line - 1)
wenzelm@56589
    76
        buffer.getFoldLevel(line - 1) - depth(range.start - 1) + depth(range.stop - 1)
wenzelm@50542
    77
      }
wenzelm@50542
    78
    }
wenzelm@50542
    79
  }
wenzelm@50542
    80
}
wenzelm@50542
    81