src/Tools/jEdit/src/pretty_text_area.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/pretty_text_area.scala
    Author:     Makarius

GUI component for pretty-printed text with markup, rendered like jEdit
text area.
*/

package isabelle.jedit


import isabelle._

import java.awt.{Color, Font, Toolkit, Window}
import java.awt.event.{InputEvent, KeyEvent}
import java.awt.im.InputMethodRequests
import javax.swing.JTextField
import javax.swing.event.{DocumentListener, DocumentEvent}

import scala.swing.{Label, Component}
import scala.util.matching.Regex

import org.gjt.sp.jedit.{jEdit, View, Registers, JEditBeanShellAction}
import org.gjt.sp.jedit.input.{DefaultInputHandlerProvider, TextAreaInputHandler}
import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
import org.gjt.sp.jedit.syntax.SyntaxStyle
import org.gjt.sp.jedit.gui.KeyEventTranslator
import org.gjt.sp.util.{SyntaxUtilities, Log}


class Pretty_Text_Area(
  view: View,
  close_action: () => Unit = () => (),
  propagate_keys: Boolean = false
) extends JEditEmbeddedTextArea {
  pretty_text_area =>

  GUI_Thread.require {}

  private var current_font_info: Font_Info = Font_Info.main()
  private var current_output: List[XML.Elem] = Nil
  private var current_base_snapshot = Document.Snapshot.init
  private var current_base_results = Command.Results.empty
  private var current_rendering: JEdit_Rendering =
    JEdit_Rendering(current_base_snapshot, Nil, Command.Results.empty)

  private val future_refresh = Synchronized[Option[Future[Unit]]](None)
  private def fork_refresh(body: => Unit): Future[Unit] =
    future_refresh.change_result({ old =>
      old.foreach(_.cancel())
      val future = Future.fork(body)
      (future, Some(future))
    })

  private val rich_text_area =
    new Rich_Text_Area(view, pretty_text_area, () => current_rendering, close_action,
      get_search_pattern _, () => (), caret_visible = false, enable_hovering = true)

  private var current_search_pattern: Option[Regex] = None
  def get_search_pattern(): Option[Regex] = GUI_Thread.require { current_search_pattern }

  def get_background(): Option[Color] = None

  def refresh(): Unit = {
    GUI_Thread.require {}

    val font = current_font_info.font
    getPainter.setFont(font)
    getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
    getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
    getPainter.setStyles(
      SyntaxUtilities.loadStyles(current_font_info.family, current_font_info.size.round))
    getPainter.setLineExtraSpacing(jEdit.getIntegerProperty("options.textarea.lineSpacing", 0))

    val fold_line_style = new Array[SyntaxStyle](4)
    for (i <- 0 to 3) {
      fold_line_style(i) =
        SyntaxUtilities.parseStyle(
          jEdit.getProperty("view.style.foldLine." + i),
          current_font_info.family, current_font_info.size.round, true)
    }
    getPainter.setFoldLineStyle(fold_line_style)

    getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
    getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
    get_background().foreach { bg => getPainter.setBackground(bg); getGutter.setBackground(bg) }
    getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor"))
    getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor"))
    getGutter.setFont(jEdit.getFontProperty("view.gutter.font"))
    getGutter.setBorder(0,
      jEdit.getColorProperty("view.gutter.focusBorderColor"),
      jEdit.getColorProperty("view.gutter.noFocusBorderColor"),
      getPainter.getBackground)
    getGutter.setFoldPainter(view.getTextArea.getFoldPainter)
    getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))

    if (getWidth > 0) {
      val metric = JEdit_Lib.font_metric(getPainter)
      val margin = Rich_Text.component_margin(metric, getPainter)
      val output = current_output
      val snapshot = current_base_snapshot
      val results = current_base_results

      lazy val current_refresh: Future[Unit] = fork_refresh(
        {
          val (rich_texts, rendering) =
            try {
              val rich_texts = Rich_Text.format(output, margin, metric, cache = PIDE.cache)
              val rendering = JEdit_Rendering(snapshot, rich_texts, results)
              (rich_texts, rendering)
            }
            catch {
              case exn: Throwable if !Exn.is_interrupt(exn) =>
                Log.log(Log.ERROR, this, exn)
                throw exn
            }

          GUI_Thread.later {
            if (future_refresh.value.contains(current_refresh)) {
              current_rendering = rendering

              val scroll_bottom = JEdit_Lib.scrollbar_bottom(pretty_text_area)
              val scroll_start = JEdit_Lib.scrollbar_start(pretty_text_area)
              val update_start =
                JEdit_Lib.buffer_edit(getBuffer) {
                  rich_text_area.active_reset()
                  getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
                  JEdit_Lib.set_text(getBuffer, rich_texts.map(_.text))
                }

              setCaretPosition(
                if (scroll_bottom) JEdit_Lib.bottom_line_offset(getBuffer)
                else if (scroll_start < update_start) scroll_start
                else 0)
              JEdit_Lib.scroll_to_caret(pretty_text_area)
            }
          }
        })
      current_refresh
    }
  }

  def resize(font_info: Font_Info): Unit = GUI_Thread.require {
    current_font_info = font_info
    refresh()
  }

  def update(
    base_snapshot: Document.Snapshot,
    base_results: Command.Results,
    output: List[XML.Elem]
  ): Unit = {
    GUI_Thread.require {}
    require(!base_snapshot.is_outdated, "document snapshot outdated")

    current_base_snapshot = base_snapshot
    current_base_results = base_results
    current_output = output.map(Protocol_Message.provide_serial)
    refresh()
  }

  def detach(): Unit = {
    GUI_Thread.require {}
    Info_Dockable(view, current_base_snapshot, current_base_results, current_output)
  }

  def detach_operation: Option[() => Unit] =
    if (current_output.isEmpty) None else Some(() => detach())


  /* search */

  private val search_label: Component = new Label("Search:") {
    tooltip = "Search and highlight output via regular expression"
  }

  private val search_field: Component =
    Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search") {
      private val input_delay =
        Delay.last(PIDE.session.input_delay, gui = true) { search_action(this) }
      getDocument.addDocumentListener(new DocumentListener {
        def changedUpdate(e: DocumentEvent): Unit = input_delay.invoke()
        def insertUpdate(e: DocumentEvent): Unit = input_delay.invoke()
        def removeUpdate(e: DocumentEvent): Unit = input_delay.invoke()
      })
      setColumns(20)
      setToolTipText(search_label.tooltip)
      setFont(GUI.imitate_font(getFont, scale = 1.2))
    })

  private val search_field_foreground = search_field.foreground

  private def search_action(text_field: JTextField): Unit = {
    val (pattern, ok) =
      text_field.getText match {
        case null | "" => (None, true)
        case s =>
          val re = Library.make_regex(s)
          (re, re.isDefined)
      }
    if (current_search_pattern != pattern) {
      current_search_pattern = pattern
      pretty_text_area.getPainter.repaint()
    }
    text_field.setForeground(
      if (ok) search_field_foreground
      else current_rendering.color(Rendering.Color.error))
  }


  /* zoom */

  val zoom_component: Font_Info.Zoom =
    new Font_Info.Zoom { override def changed(): Unit = zoom() }

  def zoom(zoom: Font_Info.Zoom = zoom_component): Unit =
    resize(Font_Info.main(scale = PIDE.options.real("jedit_font_scale"), zoom = zoom))


  /* common GUI components */

  def search_components: List[Component] = List(search_label, search_field)

  def search_zoom_components: List[Component] = List(search_label, search_field, zoom_component)


  /* key handling */

  override def getInputMethodRequests: InputMethodRequests = null

  inputHandlerProvider =
    new DefaultInputHandlerProvider(new TextAreaInputHandler(pretty_text_area) {
      override def getAction(action: String): JEditBeanShellAction =
        pretty_text_area.getActionContext.getAction(action)
      override def processKeyEvent(evt: KeyEvent, from: Int, global: Boolean): Unit = {}
      override def handleKey(key: KeyEventTranslator.Key, dry_run: Boolean): Boolean = false
    })

  addKeyListener(JEdit_Lib.key_listener(
    key_pressed = { (evt: KeyEvent) =>
      val strict_control =
        JEdit_Lib.command_modifier(evt) && !JEdit_Lib.shift_modifier(evt)

      evt.getKeyCode match {
        case KeyEvent.VK_C | KeyEvent.VK_INSERT
        if strict_control && pretty_text_area.getSelectionCount != 0 =>
          Registers.copy(pretty_text_area, '$')
          evt.consume()

        case KeyEvent.VK_A
        if strict_control =>
          pretty_text_area.selectAll()
          evt.consume()

        case KeyEvent.VK_ESCAPE =>
          if (Isabelle.dismissed_popups(view)) evt.consume()

        case _ =>
      }
      if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
    },
    key_typed = { (evt: KeyEvent) =>
      if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
    })
  )


  /* init */

  getPainter.setStructureHighlightEnabled(false)
  getPainter.setLineHighlightEnabled(false)

  getBuffer.setTokenMarker(Isabelle.mode_token_marker("isabelle-output").get)
  getBuffer.setStringProperty("noWordSep", "_'?⇩")

  rich_text_area.activate()
}