avoid auto-load dialog while exit/closeAllBuffers is active: the perspective manager happens to indicate this precisely in jEdit 5.2.0;
authorwenzelm
Tue Apr 28 11:47:49 2015 +0200 (2015-04-28)
changeset 602059ee125c3bff7
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
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Apr 27 16:46:52 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Apr 28 11:47:49 2015 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  import scala.swing.{ListView, ScrollPane}
     1.6  
     1.7 -import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug}
     1.8 +import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
     1.9  import org.jedit.options.CombinedOptions
    1.10  import org.gjt.sp.jedit.gui.AboutDialog
    1.11  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    1.12 @@ -199,7 +199,9 @@
    1.13    private lazy val delay_load =
    1.14      GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
    1.15      {
    1.16 -      if (Isabelle.continuous_checking && delay_load_activated()) {
    1.17 +      if (Isabelle.continuous_checking && delay_load_activated() &&
    1.18 +          PerspectiveManager.isPerspectiveEnabled)
    1.19 +      {
    1.20          try {
    1.21            val view = jEdit.getActiveView()
    1.22