src/Pure/GUI/rich_text.scala
author wenzelm
Tue, 12 Nov 2024 22:30:45 +0100
changeset 81433 c3793899b880
parent 81432 85fc3b482924
permissions -rw-r--r--
performance tuning: cache for Rich_Text.format, notably for incremental tracing;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
81416
206dd586f3d7 clarified modules;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/GUI/rich_text.scala
206dd586f3d7 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
206dd586f3d7 clarified modules;
wenzelm
parents:
diff changeset
     3
206dd586f3d7 clarified modules;
wenzelm
parents:
diff changeset
     4
Support for rendering of rich text, based on individual messages (XML.Elem).
206dd586f3d7 clarified modules;
wenzelm
parents:
diff changeset
     5
*/
206dd586f3d7 clarified modules;
wenzelm
parents:
diff changeset
     6
206dd586f3d7 clarified modules;
wenzelm
parents:
diff changeset
     7
package isabelle
206dd586f3d7 clarified modules;
wenzelm
parents:
diff changeset
     8
206dd586f3d7 clarified modules;
wenzelm
parents:
diff changeset
     9
81433
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    10
import java.lang.ref.WeakReference
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    11
81417
964b85e04f1f clarified margin operations (again, reverting 4794576828df);
wenzelm
parents: 81416
diff changeset
    12
import javax.swing.JComponent
964b85e04f1f clarified margin operations (again, reverting 4794576828df);
wenzelm
parents: 81416
diff changeset
    13
81418
de8dbdadda76 clarified modules;
wenzelm
parents: 81417
diff changeset
    14
import scala.collection.mutable
de8dbdadda76 clarified modules;
wenzelm
parents: 81417
diff changeset
    15
81417
964b85e04f1f clarified margin operations (again, reverting 4794576828df);
wenzelm
parents: 81416
diff changeset
    16
81416
206dd586f3d7 clarified modules;
wenzelm
parents:
diff changeset
    17
object Rich_Text {
81420
d25a241502c1 tuned comments;
wenzelm
parents: 81419
diff changeset
    18
  /* margin */
d25a241502c1 tuned comments;
wenzelm
parents: 81419
diff changeset
    19
d25a241502c1 tuned comments;
wenzelm
parents: 81419
diff changeset
    20
  def make_margin(metric: Font_Metric, margin: Int, limit: Int = -1): Int = {
d25a241502c1 tuned comments;
wenzelm
parents: 81419
diff changeset
    21
    val m = (margin * metric.average).toInt
d25a241502c1 tuned comments;
wenzelm
parents: 81419
diff changeset
    22
    (if (limit < 0) m else m min limit) max 20
d25a241502c1 tuned comments;
wenzelm
parents: 81419
diff changeset
    23
  }
d25a241502c1 tuned comments;
wenzelm
parents: 81419
diff changeset
    24
d25a241502c1 tuned comments;
wenzelm
parents: 81419
diff changeset
    25
  def component_margin(metric: Font_Metric, component: JComponent): Int =
d25a241502c1 tuned comments;
wenzelm
parents: 81419
diff changeset
    26
    make_margin(metric, (component.getWidth.toDouble / metric.average_width).toInt)
d25a241502c1 tuned comments;
wenzelm
parents: 81419
diff changeset
    27
d25a241502c1 tuned comments;
wenzelm
parents: 81419
diff changeset
    28
d25a241502c1 tuned comments;
wenzelm
parents: 81419
diff changeset
    29
  /* format */
d25a241502c1 tuned comments;
wenzelm
parents: 81419
diff changeset
    30
81432
85fc3b482924 clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages;
wenzelm
parents: 81428
diff changeset
    31
  sealed case class Formatted(id: Document_ID.Generic, body: XML.Body) {
81421
8c1680ac4160 clarified signature and data storage: incremental lazy values;
wenzelm
parents: 81420
diff changeset
    32
    lazy val text: String = XML.content(body)
81432
85fc3b482924 clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages;
wenzelm
parents: 81428
diff changeset
    33
    lazy val markups: Command.Markups = Command.Markups.init(Markup_Tree.from_XML(body))
85fc3b482924 clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages;
wenzelm
parents: 81428
diff changeset
    34
    def command(results: Command.Results): Command =
85fc3b482924 clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages;
wenzelm
parents: 81428
diff changeset
    35
      Command.unparsed(text, id = id, results = results, markups = markups)
81416
206dd586f3d7 clarified modules;
wenzelm
parents:
diff changeset
    36
  }
81417
964b85e04f1f clarified margin operations (again, reverting 4794576828df);
wenzelm
parents: 81416
diff changeset
    37
81433
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    38
  def format(
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    39
    msgs: List[XML.Elem],
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    40
    margin: Double,
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    41
    metric: Font_Metric,
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    42
    cache: Cache = Cache.none
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    43
  ): List[Formatted] = {
81421
8c1680ac4160 clarified signature and data storage: incremental lazy values;
wenzelm
parents: 81420
diff changeset
    44
    val result = new mutable.ListBuffer[Formatted]
81418
de8dbdadda76 clarified modules;
wenzelm
parents: 81417
diff changeset
    45
    for (msg <- msgs) {
81432
85fc3b482924 clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages;
wenzelm
parents: 81428
diff changeset
    46
      if (result.nonEmpty) result += Formatted(Document_ID.make(), Pretty.Separator)
81433
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    47
      result += cache.format(msg, margin, metric)
81418
de8dbdadda76 clarified modules;
wenzelm
parents: 81417
diff changeset
    48
      Exn.Interrupt.expose()
de8dbdadda76 clarified modules;
wenzelm
parents: 81417
diff changeset
    49
    }
de8dbdadda76 clarified modules;
wenzelm
parents: 81417
diff changeset
    50
    result.toList
de8dbdadda76 clarified modules;
wenzelm
parents: 81417
diff changeset
    51
  }
81428
257ec066b360 clarified signature and modules;
wenzelm
parents: 81424
diff changeset
    52
257ec066b360 clarified signature and modules;
wenzelm
parents: 81424
diff changeset
    53
  def formatted_lines(formatted: List[Formatted]): Int =
257ec066b360 clarified signature and modules;
wenzelm
parents: 81424
diff changeset
    54
    if (formatted.isEmpty) 0
257ec066b360 clarified signature and modules;
wenzelm
parents: 81424
diff changeset
    55
    else {
257ec066b360 clarified signature and modules;
wenzelm
parents: 81424
diff changeset
    56
      1 + formatted.iterator.map(form =>
257ec066b360 clarified signature and modules;
wenzelm
parents: 81424
diff changeset
    57
        XML.traverse_text(form.body, 0, (n, s) => n + Library.count_newlines(s))).sum
257ec066b360 clarified signature and modules;
wenzelm
parents: 81424
diff changeset
    58
    }
257ec066b360 clarified signature and modules;
wenzelm
parents: 81424
diff changeset
    59
257ec066b360 clarified signature and modules;
wenzelm
parents: 81424
diff changeset
    60
  def formatted_margin(metric: Font_Metric, formatted: List[Formatted]): Double =
257ec066b360 clarified signature and modules;
wenzelm
parents: 81424
diff changeset
    61
    split_lines(formatted.map(_.text).mkString)
257ec066b360 clarified signature and modules;
wenzelm
parents: 81424
diff changeset
    62
      .foldLeft(0.0) { case (m, line) => m max metric(line) }
81433
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    63
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    64
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    65
  /* cache */
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    66
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    67
  object Cache {
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    68
    def make(
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    69
        compress: Compress.Cache = Compress.Cache.make(),
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    70
        max_string: Int = isabelle.Cache.default_max_string,
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    71
        initial_size: Int = isabelle.Cache.default_initial_size): Cache =
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    72
      new Cache(compress, initial_size, max_string)
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    73
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    74
    val none: Cache = make(max_string = 0)
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    75
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    76
    sealed case class Args(msg: XML.Elem, margin: Double, metric: Font_Metric)
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    77
  }
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    78
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    79
  class Cache(compress: Compress.Cache, max_string: Int, initial_size: Int)
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    80
  extends Term.Cache(compress, max_string, initial_size) {
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    81
    cache =>
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    82
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    83
    def format(msg: XML.Elem, margin: Double, metric: Font_Metric): Formatted = {
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    84
      def run: Formatted =
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    85
        Formatted(Protocol_Message.get_serial(msg),
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    86
          cache.body(Pretty.formatted(List(msg), margin = margin, metric = metric)))
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    87
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    88
      if (cache.table == null) run
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    89
      else {
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    90
        val x = Cache.Args(msg, margin, metric)
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    91
        cache.table.get(x) match {
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    92
          case ref: WeakReference[Any] => ref.get.asInstanceOf[Formatted]
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    93
          case null =>
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    94
            val y = run
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    95
            cache.table.synchronized {
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    96
              if (cache.table.get(x) == null) cache.table.put(x, new WeakReference[Any](y))
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    97
            }
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    98
            y
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
    99
        }
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
   100
      }
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
   101
    }
c3793899b880 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm
parents: 81432
diff changeset
   102
  }
81416
206dd586f3d7 clarified modules;
wenzelm
parents:
diff changeset
   103
}