--- a/src/Tools/jEdit/src/document_model.scala Thu Jul 15 21:35:31 2021 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Thu Jul 15 22:07:56 2021 +0200
@@ -80,6 +80,8 @@
private val state = Synchronized(State()) // owned by GUI thread
+ def reset(): Unit = state.change(_ => State())
+
def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
def get(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)