# HG changeset patch
# User wenzelm
# Date 1672139747 -3600
# Node ID 7a0438979e8580332c64857838b4b95a0fefb645
# Parent  27a8e9e8761eb7fcd7923ab0d35111addb047126
clarified signature: avoid case class with mutable state;

diff -r 27a8e9e8761e -r 7a0438979e85 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Dec 27 12:00:37 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Dec 27 12:15:47 2022 +0100
@@ -53,7 +53,7 @@
           case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit())
           case _ => None
         }
-      val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model)
+      val buffer_model = Buffer_Model.init(old_model, session, node_name, buffer)
       (buffer_model,
         copy(models = models + (node_name -> buffer_model),
           buffer_models = buffer_models + (buffer -> buffer_model)))
@@ -485,8 +485,20 @@
   def is_stable: Boolean = pending_edits.isEmpty
 }
 
-case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
-extends Document_Model {
+object Buffer_Model {
+  def init(
+    old_model: Option[File_Model],
+    session: Session,
+    node_name: Document.Node.Name,
+    buffer: Buffer
+  ): Buffer_Model = (new Buffer_Model(session, node_name, buffer)).init(old_model)
+}
+
+class Buffer_Model private(
+  val session: Session,
+  val node_name: Document.Node.Name,
+  val buffer: Buffer
+) extends Document_Model {
   /* text */
 
   def get_text(range: Text.Range): Option[String] =