# HG changeset patch # User wenzelm # Date 1405877806 -7200 # Node ID b79b75f92604acf3a377c6dafd1bf543ee92507a # Parent 74bbe9317aa4dfcdad3b4c9acd248379212a6576 avoid delay_load overrun; diff -r 74bbe9317aa4 -r b79b75f92604 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Sun Jul 20 17:54:01 2014 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Sun Jul 20 19:36:46 2014 +0200 @@ -191,54 +191,61 @@ PIDE.init_models() } + private val delay_load_active = Synchronized(false) + private def delay_load_activated(): Boolean = + delay_load_active.guarded_access(a => Some((!a, true))) + private lazy val delay_load = Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) { - if (Isabelle.continuous_checking) { - val view = jEdit.getActiveView() + if (Isabelle.continuous_checking && delay_load_activated()) { + try { + val view = jEdit.getActiveView() - val buffers = JEdit_Lib.jedit_buffers().toList - if (buffers.forall(_.isLoaded)) { - def loaded_buffer(name: String): Boolean = - buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name) + val buffers = JEdit_Lib.jedit_buffers().toList + if (buffers.forall(_.isLoaded)) { + def loaded_buffer(name: String): Boolean = + buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name) - val thys = - for { - buffer <- buffers - model <- PIDE.document_model(buffer) - if model.is_theory - } yield (model.node_name, Position.none) + val thys = + for { + buffer <- buffers + model <- PIDE.document_model(buffer) + if model.is_theory + } yield (model.node_name, Position.none) - val thy_info = new Thy_Info(PIDE.resources) - // FIXME avoid I/O in Swing thread!?! - val files = thy_info.dependencies("", thys).deps.map(_.name.node). - filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file)) + val thy_info = new Thy_Info(PIDE.resources) + // FIXME avoid I/O in Swing thread!?! + val files = thy_info.dependencies("", thys).deps.map(_.name.node). + filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file)) - if (!files.isEmpty) { - if (PIDE.options.bool("jedit_auto_load")) { - files.foreach(file => jEdit.openFile(null: View, file)) - } - else { - val files_list = new ListView(files.sorted) - for (i <- 0 until files.length) - files_list.selection.indices += i + if (!files.isEmpty) { + if (PIDE.options.bool("jedit_auto_load")) { + files.foreach(file => jEdit.openFile(null: View, file)) + } + else { + val files_list = new ListView(files.sorted) + for (i <- 0 until files.length) + files_list.selection.indices += i - val answer = - GUI.confirm_dialog(view, - "Auto loading of required files", - JOptionPane.YES_NO_OPTION, - "The following files are required to resolve theory imports.", - "Reload selected files now?", - new ScrollPane(files_list), - new Isabelle.Continuous_Checking) - if (answer == 0) { - files.foreach(file => - if (files_list.selection.items.contains(file)) - jEdit.openFile(null: View, file)) + val answer = + GUI.confirm_dialog(view, + "Auto loading of required files", + JOptionPane.YES_NO_OPTION, + "The following files are required to resolve theory imports.", + "Reload selected files now?", + new ScrollPane(files_list), + new Isabelle.Continuous_Checking) + if (answer == 0) { + files.foreach(file => + if (files_list.selection.items.contains(file)) + jEdit.openFile(null: View, file)) + } } } } } + finally { delay_load_active.change(_ => false) } } }