src/Tools/jEdit/src/fold_handling.scala

more rebust mechanics of refresh (see also 82110cbcf9a1 and 2d9b6e32632d): painter.getFontRenderContext might be in undefined state (notably on macOS due to display scaling);

/*  Title:      Tools/jEdit/src/fold_handling.scala
    Author:     Makarius

Handling of folds within the text structure.
*/

package isabelle.jedit


import isabelle._

import java.util.{List => JList}

import javax.swing.text.Segment

import scala.jdk.CollectionConverters._

import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler}


object Fold_Handling {
  /* input: dynamic line context  */

  class Fold_Handler extends FoldHandler("isabelle") {
    override def equals(other: Any): Boolean =
      other match {
        case that: Fold_Handler => true
        case _ => false
      }

    override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
      Token_Markup.Line_Context.after(buffer, line).structure.depth max 0

    override def getPrecedingFoldLevels(
      buffer: JEditBuffer,
      line: Int,
      seg: Segment, level: Int
    ): JList[Integer] = {
      val structure = Token_Markup.Line_Context.after(buffer, line).structure
      val result =
        if (line > 0 && structure.command)
          Range.inclusive(line - 1, 0, -1).iterator.
            map(i => Token_Markup.Line_Context.after(buffer, i).structure).
            takeWhile(_.improper).map(_ => structure.depth max 0).toList
        else Nil

      if (result.isEmpty) null else result.map(Integer.valueOf).asJava
    }
  }


  /* output: static document rendering */

  class Document_Fold_Handler(private val rendering: JEdit_Rendering)
  extends FoldHandler("isabelle-document") {
    override def equals(other: Any): Boolean =
      other match {
        case that: Document_Fold_Handler => this.rendering == that.rendering
        case _ => false
      }

    override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int = {
      def depth(i: Text.Offset): Int =
        if (i < 0) 0
        else {
          rendering.fold_depth(Text.Range(i, i + 1)) match {
            case Text.Info(_, d) :: _ => d
            case _ => 0
          }
        }

      if (line <= 0) 0
      else {
        val range = JEdit_Lib.line_range(buffer, line - 1)
        buffer.getFoldLevel(line - 1) - depth(range.start - 1) + depth(range.stop - 1)
      }
    }
  }
}