<commit_before>/*  Title:      Tools/jEdit/src/document_model.scala
    Author:     <NAME>, TU Munich
    Author:     Makarius

Document model connected to jEdit buffer -- single node in theory graph.
*/

package isabelle.jedit


import isabelle._

import scala.collection.mutable

import org.gjt.sp.jedit.Buffer
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
import org.gjt.sp.jedit.textarea.TextArea

import java.awt.font.TextAttribute


object Document_Model
{
  /* document model of buffer */

  private val key = "isabelle.document_model"

  def apply(buffer: Buffer): Option[Document_Model] =
  {
    Swing_Thread.require()
    buffer.getProperty(key) match {
      case model: Document_Model => Some(model)
      case _ => None
    }
  }

  def exit(buffer: Buffer)
  {
    Swing_Thread.require()
    apply(buffer) match {
      case None =>
      case Some(model) =>
        model.deactivate()
        buffer.unsetProperty(key)
    }
  }

  def init(session: Session, buffer: Buffer,
    master_dir: String, node_name: String, thy_name: String): Document_Model =
  {
    exit(buffer)
    val model = new Document_Model(session, buffer, master_dir, node_name, thy_name)
    buffer.setProperty(key, model)
    model.activate()
    model
  }
}


class Document_Model(val session: Session, val buffer: Buffer,
  val master_dir: String, val node_name: String, val thy_name: String)
{
  /* header */

  def node_header(): Exn.Result[Thy_Header] =
  {
    Swing_Thread.require()
    Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }
  }


  /* perspective */

  def perspective(): Text.Perspective =
  {
    Swing_Thread.require()
    Text.perspective(
      for {
        doc_view <- Isabelle.document_views(buffer)
        range <- doc_view.perspective()
      } yield range)
  }


  /* pending text edits */

  private object pending_edits  // owned by Swing thread
  {
    private val pending = new mutable.ListBuffer[Text.Edit]
    private var pending_perspective = false
    def snapshot(): List[Text.Edit] = pending.toList

    def flush()
    {
      Swing_Thread.require()
      snapshot() match {
        case Nil if !pending_perspective =>
        case edits =>
          pending.clear
          pending_perspective = false
          session.edit_node(node_name, master_dir, node_header(), perspective(), edits)
      }
    }

    def init()<commit_msg>early filtering of unchanged perspective;<commit_after>/*  Title:      Tools/jEdit/src/document_model.scala
    Author:     <NAME>, <NAME>
    Author:     Makarius

Document model connected to jEdit buffer -- single node in theory graph.
*/

package isabelle.jedit


import isabelle._

import scala.collection.mutable

import org.gjt.sp.jedit.Buffer
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
import org.gjt.sp.jedit.textarea.TextArea

import java.awt.font.TextAttribute


object Document_Model
{
  /* document model of buffer */

  private val key = "isabelle.document_model"

  def apply(buffer: Buffer): Option[Document_Model] =
  {
    Swing_Thread.require()
    buffer.getProperty(key) match {
      case model: Document_Model => Some(model)
      case _ => None
    }
  }

  def exit(buffer: Buffer)
  {
    Swing_Thread.require()
    apply(buffer) match {
      case None =>
      case Some(model) =>
        model.deactivate()
        buffer.unsetProperty(key)
    }
  }

  def init(session: Session, buffer: Buffer,
    master_dir: String, node_name: String, thy_name: String): Document_Model =
  {
    exit(buffer)
    val model = new Document_Model(session, buffer, master_dir, node_name, thy_name)
    buffer.setProperty(key, model)
    model.activate()
    model
  }
}


class Document_Model(val session: Session, val buffer: Buffer,
  val master_dir: String, val node_name: String, val thy_name: String)
{
  /* header */

  def node_header(): Exn.Result[Thy_Header] =
  {
    Swing_Thread.require()
    Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }
  }


  /* perspective */

  def perspective(): Text.Perspective =
  {
    Swing_Thread.require()
    Text.perspective(
      for {
        doc_view <- Isabelle.document_views(buffer)
        range <- doc_view.perspective()
      } yield range)
  }


  /* pending text edits */

  private object pending_edits  // owned by Swing thread
  {
    private val pending = new mutable.ListBuffer[Text.Edit]
    private var pending_perspective = false
    private var last_perspective: Text.Perspective = Nil

    def snapshot(): List[Text.Edit] = pending.toList

    def flush()
    {
      Swing_Thread.require()

      val new_perspective =
        if (pending_perspective) { pending_perspective = false; perspective() }
        else last_perspective

      snapshot() match {
        case Nil if new_perspective == last_perspective =>
        case edits =>
          pending.clear
          last_perspective = new_perspective
          session.edit_node(node_name, master_dir, node_header(), new_perspective, edits)
      }
    }

    def init()
{'fraction_non_alphanumeric': 0.10272495589100177, 'fraction_numerical': 0.00039207998431680063, 'mean_word_length': 2.951975213013168, 'pattern_counts': {'":': 0, '<': 10, '<?xml version=': 0, '>': 18, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1873390', 'n_tokens_mistral': 1622, 'n_tokens_neox': 1570, 'n_words': 373}