src/Tools/jEdit/src/plugin.scala
changeset 60205 9ee125c3bff7
parent 60075 b079ee0e766c
child 60206 18267ceb10b5
equal deleted inserted replaced
60204:137b3fc46bb3 60205:9ee125c3bff7
    11 
    11 
    12 import javax.swing.JOptionPane
    12 import javax.swing.JOptionPane
    13 
    13 
    14 import scala.swing.{ListView, ScrollPane}
    14 import scala.swing.{ListView, ScrollPane}
    15 
    15 
    16 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug}
    16 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
    17 import org.jedit.options.CombinedOptions
    17 import org.jedit.options.CombinedOptions
    18 import org.gjt.sp.jedit.gui.AboutDialog
    18 import org.gjt.sp.jedit.gui.AboutDialog
    19 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    19 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    20 import org.gjt.sp.jedit.buffer.JEditBuffer
    20 import org.gjt.sp.jedit.buffer.JEditBuffer
    21 import org.gjt.sp.jedit.syntax.ModeProvider
    21 import org.gjt.sp.jedit.syntax.ModeProvider
   197     delay_load_active.guarded_access(a => Some((!a, true)))
   197     delay_load_active.guarded_access(a => Some((!a, true)))
   198 
   198 
   199   private lazy val delay_load =
   199   private lazy val delay_load =
   200     GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
   200     GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
   201     {
   201     {
   202       if (Isabelle.continuous_checking && delay_load_activated()) {
   202       if (Isabelle.continuous_checking && delay_load_activated() &&
       
   203           PerspectiveManager.isPerspectiveEnabled)
       
   204       {
   203         try {
   205         try {
   204           val view = jEdit.getActiveView()
   206           val view = jEdit.getActiveView()
   205 
   207 
   206           val buffers = JEdit_Lib.jedit_buffers().toList
   208           val buffers = JEdit_Lib.jedit_buffers().toList
   207           if (buffers.forall(_.isLoaded)) {
   209           if (buffers.forall(_.isLoaded)) {