# 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] =