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