--- 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(),
--- 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)
--- 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)
--- 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