# HG changeset patch # User wenzelm # Date 1452010474 -3600 # Node ID 500f54190a3ce38eb7507f9fda03841eaa0ab3ec # Parent d9874039786e167abe87d23942a899380bbcdff8 more robust event propagation; diff -r d9874039786e -r 500f54190a3c src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Tue Jan 05 15:53:17 2016 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Tue Jan 05 17:14:34 2016 +0100 @@ -37,8 +37,8 @@ @volatile var plugin: Plugin = null @volatile var session: Session = new Session(JEdit_Resources.empty) - def options_changed() { plugin.options_changed() } - def deps_changed() { plugin.deps_changed() } + def options_changed() { if (plugin != null) plugin.options_changed() } + def deps_changed() { if (plugin != null) plugin.deps_changed() } def resources(): JEdit_Resources = session.resources.asInstanceOf[JEdit_Resources] @@ -110,16 +110,19 @@ for { buffer <- JEdit_Lib.jedit_buffers() - if buffer != null && !buffer.isLoading && !buffer.getBooleanProperty(Buffer.GZIPPED) + if buffer != null && !buffer.getBooleanProperty(Buffer.GZIPPED) } { - JEdit_Lib.buffer_lock(buffer) { - val node_name = resources.node_name(buffer) - val model = Document_Model.init(session, buffer, node_name, document_model(buffer)) - for { - text_area <- JEdit_Lib.jedit_text_areas(buffer) - if document_view(text_area).map(_.model) != Some(model) - } Document_View.init(model, text_area) + if (buffer.isLoaded) { + JEdit_Lib.buffer_lock(buffer) { + val node_name = resources.node_name(buffer) + val model = Document_Model.init(session, buffer, node_name, document_model(buffer)) + for { + text_area <- JEdit_Lib.jedit_text_areas(buffer) + if document_view(text_area).map(_.model) != Some(model) + } Document_View.init(model, text_area) + } } + else if (plugin != null) plugin.delay_init.invoke() } PIDE.editor.invoke() @@ -184,7 +187,7 @@ /* theory files */ - private lazy val delay_init = + lazy val delay_init = GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) { PIDE.init_models() @@ -193,73 +196,75 @@ 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 = - GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) + private def delay_load_action() + { + if (Isabelle.continuous_checking && delay_load_activated() && + PerspectiveManager.isPerspectiveEnabled) { - if (Isabelle.continuous_checking && delay_load_activated() && - PerspectiveManager.isPerspectiveEnabled) - { - try { - val view = jEdit.getActiveView() + 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) - val thy_files = thy_info.dependencies("", thys).deps.map(_.name.node) + val thy_info = new Thy_Info(PIDE.resources) + val thy_files = thy_info.dependencies("", thys).deps.map(_.name.node) - val aux_files = - if (PIDE.options.bool("jedit_auto_resolve")) { - PIDE.editor.stable_tip_version() match { - case Some(version) => PIDE.resources.undefined_blobs(version.nodes).map(_.node) - case None => Nil - } - } - else Nil - - val files = - (thy_files ::: aux_files).filter(file => - !loaded_buffer(file) && PIDE.resources.check_file(file)) - - if (files.nonEmpty) { - if (PIDE.options.bool("jedit_auto_load")) { - files.foreach(file => jEdit.openFile(null: View, file)) + val aux_files = + if (PIDE.options.bool("jedit_auto_resolve")) { + PIDE.editor.stable_tip_version() match { + case Some(version) => PIDE.resources.undefined_blobs(version.nodes).map(_.node) + case None => Nil } - else { - val files_list = new ListView(files.sorted) - for (i <- 0 until files.length) - files_list.selection.indices += i + } + else Nil + + val files = + (thy_files ::: aux_files).filter(file => + !loaded_buffer(file) && PIDE.resources.check_file(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)) - } + if (files.nonEmpty) { + 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)) } } } } - finally { delay_load_active.change(_ => false) } + else delay_load.invoke() } + finally { delay_load_active.change(_ => false) } } + } + + lazy val delay_load = + GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) { delay_load_action() } /* session phase */