# HG changeset patch # User wenzelm # Date 1670496935 -3600 # Node ID 01978b4acdafb9d88087697b50629fa8df38f27a # Parent 2ccad59c0d4d79c150c9000a95179c3a8722a95d tuned; diff -r 2ccad59c0d4d -r 01978b4acdaf src/Tools/jEdit/src/jedit_resources.scala --- a/src/Tools/jEdit/src/jedit_resources.scala Thu Dec 08 11:51:42 2022 +0100 +++ b/src/Tools/jEdit/src/jedit_resources.scala Thu Dec 08 11:55:35 2022 +0100 @@ -131,12 +131,13 @@ /* theory text edits */ + def auto_resolve: Boolean = PIDE.options.bool("jedit_auto_resolve") + override def commit(change: Session.Change): Unit = { if (change.syntax_changed.nonEmpty) { GUI_Thread.later { Document_Model.syntax_changed(change.syntax_changed) } } - if (change.deps_changed || - PIDE.options.bool("jedit_auto_resolve") && undefined_blobs(change.version).nonEmpty) { + if (change.deps_changed || auto_resolve && undefined_blobs(change.version).nonEmpty) { PIDE.plugin.deps_changed() } } diff -r 2ccad59c0d4d -r 01978b4acdaf src/Tools/jEdit/src/main_plugin.scala --- a/src/Tools/jEdit/src/main_plugin.scala Thu Dec 08 11:51:42 2022 +0100 +++ b/src/Tools/jEdit/src/main_plugin.scala Thu Dec 08 11:55:35 2022 +0100 @@ -117,7 +117,7 @@ val thy_files = resources.resolve_dependencies(models, Nil) val aux_files = - if (options.bool("jedit_auto_resolve")) { + if (resources.auto_resolve) { session.stable_tip_version(models) match { case Some(version) => resources.undefined_blobs(version) case None => delay_load.invoke(); Nil