avoid auto-load dialog while exit/closeAllBuffers is active: the perspective manager happens to indicate this precisely in jEdit 5.2.0;
authorwenzelm
Tue, 28 Apr 2015 11:47:49 +0200
changeset 60205 9ee125c3bff7
parent 60204 137b3fc46bb3
child 60206 18267ceb10b5
avoid auto-load dialog while exit/closeAllBuffers is active: the perspective manager happens to indicate this precisely in jEdit 5.2.0;
src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Apr 27 16:46:52 2015 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Apr 28 11:47:49 2015 +0200
@@ -13,7 +13,7 @@
 
 import scala.swing.{ListView, ScrollPane}
 
-import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug}
+import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
 import org.jedit.options.CombinedOptions
 import org.gjt.sp.jedit.gui.AboutDialog
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
@@ -199,7 +199,9 @@
   private lazy val delay_load =
     GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
     {
-      if (Isabelle.continuous_checking && delay_load_activated()) {
+      if (Isabelle.continuous_checking && delay_load_activated() &&
+          PerspectiveManager.isPerspectiveEnabled)
+      {
         try {
           val view = jEdit.getActiveView()