# 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()
   }
 }