clarified global state: allow to deactivate main plugin;
authorwenzelm
Thu, 15 Jul 2021 22:07:56 +0200
changeset 73999 6b213c0115f5
parent 73998 b3f2da6bef51
child 74000 4313e6c9969a
clarified global state: allow to deactivate main plugin;
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/main_plugin.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)
--- 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()
   }
 }