# HG changeset patch
# User wenzelm
# Date 1750848695 -7200
# Node ID da8ad15919851ef1d372226314c6924ec287f88a
# Parent  a07ca02ac456e72d8c146c64a1c454c057661d50
more accurate ML_Settings from underlying Session;

diff -r a07ca02ac456 -r da8ad1591985 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Wed Jun 25 12:43:37 2025 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala	Wed Jun 25 12:51:35 2025 +0200
@@ -52,8 +52,7 @@
   def options: JEdit_Options = plugin.options
   def session: JEdit_Session = plugin.session
   def resources: JEdit_Resources = session.resources
-
-  def ml_settings: ML_Settings = ML_Settings(plugin.startup_options)
+  def ml_settings: ML_Settings = session.store.ml_settings
 
   object editor extends JEdit_Editor
 }