# HG changeset patch
# User wenzelm
# Date 1731447045 -3600
# Node ID c3793899b8805f98274d426f794645c1f74fe1df
# Parent  85fc3b482924cf3a242cfc2a14417c811d346a38
performance tuning: cache for Rich_Text.format, notably for incremental tracing;

diff -r 85fc3b482924 -r c3793899b880 src/Pure/GUI/rich_text.scala
--- a/src/Pure/GUI/rich_text.scala	Tue Nov 12 11:32:07 2024 +0100
+++ b/src/Pure/GUI/rich_text.scala	Tue Nov 12 22:30:45 2024 +0100
@@ -7,6 +7,8 @@
 package isabelle
 
 
+import java.lang.ref.WeakReference
+
 import javax.swing.JComponent
 
 import scala.collection.mutable
@@ -33,15 +35,16 @@
       Command.unparsed(text, id = id, results = results, markups = markups)
   }
 
-  def format(msgs: List[XML.Elem], margin: Double, metric: Font_Metric): List[Formatted] = {
+  def format(
+    msgs: List[XML.Elem],
+    margin: Double,
+    metric: Font_Metric,
+    cache: Cache = Cache.none
+  ): List[Formatted] = {
     val result = new mutable.ListBuffer[Formatted]
     for (msg <- msgs) {
       if (result.nonEmpty) result += Formatted(Document_ID.make(), Pretty.Separator)
-
-      val id = Protocol_Message.get_serial(msg)
-      val body = Pretty.formatted(List(msg), margin = margin, metric = metric)
-      result += Formatted(id, body)
-
+      result += cache.format(msg, margin, metric)
       Exn.Interrupt.expose()
     }
     result.toList
@@ -57,4 +60,44 @@
   def formatted_margin(metric: Font_Metric, formatted: List[Formatted]): Double =
     split_lines(formatted.map(_.text).mkString)
       .foldLeft(0.0) { case (m, line) => m max metric(line) }
+
+
+  /* cache */
+
+  object Cache {
+    def make(
+        compress: Compress.Cache = Compress.Cache.make(),
+        max_string: Int = isabelle.Cache.default_max_string,
+        initial_size: Int = isabelle.Cache.default_initial_size): Cache =
+      new Cache(compress, initial_size, max_string)
+
+    val none: Cache = make(max_string = 0)
+
+    sealed case class Args(msg: XML.Elem, margin: Double, metric: Font_Metric)
+  }
+
+  class Cache(compress: Compress.Cache, max_string: Int, initial_size: Int)
+  extends Term.Cache(compress, max_string, initial_size) {
+    cache =>
+
+    def format(msg: XML.Elem, margin: Double, metric: Font_Metric): Formatted = {
+      def run: Formatted =
+        Formatted(Protocol_Message.get_serial(msg),
+          cache.body(Pretty.formatted(List(msg), margin = margin, metric = metric)))
+
+      if (cache.table == null) run
+      else {
+        val x = Cache.Args(msg, margin, metric)
+        cache.table.get(x) match {
+          case ref: WeakReference[Any] => ref.get.asInstanceOf[Formatted]
+          case null =>
+            val y = run
+            cache.table.synchronized {
+              if (cache.table.get(x) == null) cache.table.put(x, new WeakReference[Any](y))
+            }
+            y
+        }
+      }
+    }
+  }
 }
diff -r 85fc3b482924 -r c3793899b880 src/Pure/General/cache.scala
--- a/src/Pure/General/cache.scala	Tue Nov 12 11:32:07 2024 +0100
+++ b/src/Pure/General/cache.scala	Tue Nov 12 22:30:45 2024 +0100
@@ -26,9 +26,9 @@
 class Cache(max_string: Int, initial_size: Int) {
   val no_cache: Boolean = max_string == 0
 
-  private val table: JMap[Any, WeakReference[Any]] =
+  protected val table: JMap[Any, WeakReference[Any]] =
     if (max_string == 0) null
-    else  Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
+    else Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size))
 
   override def toString: String =
     if (no_cache) "Cache.none" else "Cache(size = " + table.size + ")"
diff -r 85fc3b482924 -r c3793899b880 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Tue Nov 12 11:32:07 2024 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Tue Nov 12 22:30:45 2024 +0100
@@ -53,6 +53,7 @@
   def options: JEdit_Options = plugin.options
   def resources: JEdit_Resources = plugin.resources
   def session: Session = plugin.session
+  def cache: Rich_Text.Cache = session.cache.asInstanceOf[Rich_Text.Cache]
 
   object editor extends JEdit_Editor
 }
@@ -76,7 +77,12 @@
   /* session */
 
   private var _session: Session = null
-  private def init_session(): Unit = _session = new Session(options.value, resources)
+  private def init_session(): Unit = {
+    _session =
+      new Session(options.value, resources) {
+        override val cache: Term.Cache = Rich_Text.Cache.make()
+      }
+  }
   def session: Session = _session
 
 
diff -r 85fc3b482924 -r c3793899b880 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Nov 12 11:32:07 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Nov 12 22:30:45 2024 +0100
@@ -98,7 +98,7 @@
         Some(Future.fork {
           val (rich_texts, rendering) =
             try {
-              val rich_texts = Rich_Text.format(output, margin, metric)
+              val rich_texts = Rich_Text.format(output, margin, metric, cache = PIDE.cache)
               val rendering = JEdit_Rendering(snapshot, rich_texts, results)
               (rich_texts, rendering)
             }
diff -r 85fc3b482924 -r c3793899b880 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Nov 12 11:32:07 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Nov 12 22:30:45 2024 +0100
@@ -251,7 +251,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)
+      val formatted = Rich_Text.format(output, margin, metric, cache = PIDE.cache)
       val lines = Rich_Text.formatted_lines(formatted)
 
       val h = painter.getLineHeight * lines + geometry.deco_height