# HG changeset patch
# User wenzelm
# Date 1750791645 -7200
# Node ID 535e6012ee11522661a76bcb6daea950dbf7173f
# Parent  ef9075e41a675e2441f03e268a6c8e4e83e7c511
clarified signature;

diff -r ef9075e41a67 -r 535e6012ee11 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Jun 24 20:57:27 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Jun 24 21:00:45 2025 +0200
@@ -47,7 +47,7 @@
   /* database store */
 
   def sessions_store(options: Options = PIDE.options.value): Store =
-    Store(session_options(options), cache = PIDE.cache)
+    Store(session_options(options), cache = PIDE.session.cache)
 
   def open_session_context(
     store: Store = sessions_store(),
diff -r ef9075e41a67 -r 535e6012ee11 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Tue Jun 24 20:57:27 2025 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala	Tue Jun 24 21:00:45 2025 +0200
@@ -52,7 +52,6 @@
   def options: JEdit_Options = plugin.options
   def session: JEdit_Session = plugin.session
   def resources: JEdit_Resources = session.resources
-  def cache: Rich_Text.Cache = session.cache.asInstanceOf[Rich_Text.Cache]
 
   def ml_settings: ML_Settings = ML_Settings.system(plugin.startup_options)
 
diff -r ef9075e41a67 -r 535e6012ee11 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Jun 24 20:57:27 2025 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Jun 24 21:00:45 2025 +0200
@@ -184,7 +184,7 @@
         {
           val (rich_texts, rendering) =
             try {
-              val rich_texts = Rich_Text.format(output, margin, metric, cache = PIDE.cache)
+              val rich_texts = Rich_Text.format(output, margin, metric, cache = PIDE.session.cache)
               val rendering =
                 JEdit_Rendering.make(snapshot, rich_texts = rich_texts, results = results)
               (rich_texts, rendering)
diff -r ef9075e41a67 -r 535e6012ee11 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Jun 24 20:57:27 2025 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Jun 24 21:00:45 2025 +0200
@@ -252,7 +252,7 @@
         Rich_Text.make_margin(metric, rendering.tooltip_margin,
           limit = ((w_max - geometry.deco_width) / metric.average_width).toInt)
 
-      val formatted = Rich_Text.format(output, margin, metric, cache = PIDE.cache)
+      val formatted = Rich_Text.format(output, margin, metric, cache = PIDE.session.cache)
       val lines = Rich_Text.formatted_lines(formatted)
 
       val h = painter.getLineHeight * lines + geometry.deco_height