# HG changeset patch # User wenzelm # Date 1626379676 -7200 # Node ID 6b213c0115f5bb13f9252c4ba170f922844b0d18 # Parent b3f2da6bef51ffeaa7f8827a50f1a744cf33316b clarified global state: allow to deactivate main plugin; diff -r b3f2da6bef51 -r 6b213c0115f5 src/Tools/jEdit/src/document_model.scala --- 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) diff -r b3f2da6bef51 -r 6b213c0115f5 src/Tools/jEdit/src/main_plugin.scala --- a/src/Tools/jEdit/src/main_plugin.scala Thu Jul 15 21:35:31 2021 +0200 +++ b/src/Tools/jEdit/src/main_plugin.scala Thu Jul 15 22:07:56 2021 +0200 @@ -495,5 +495,7 @@ session.stop() file_watcher.shutdown() PIDE.editor.shutdown() + + Document_Model.reset() } }