author | wenzelm |
Tue, 12 Nov 2024 22:30:45 +0100 | |
changeset 81433 | c3793899b880 |
parent 81432 | 85fc3b482924 |
permissions | -rw-r--r-- |
81416 | 1 |
/* Title: Pure/GUI/rich_text.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Support for rendering of rich text, based on individual messages (XML.Elem). |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
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 | 14 |
import scala.collection.mutable |
15 |
||
81417
964b85e04f1f
clarified margin operations (again, reverting 4794576828df);
wenzelm
parents:
81416
diff
changeset
|
16 |
|
81416 | 17 |
object Rich_Text { |
81420 | 18 |
/* margin */ |
19 |
||
20 |
def make_margin(metric: Font_Metric, margin: Int, limit: Int = -1): Int = { |
|
21 |
val m = (margin * metric.average).toInt |
|
22 |
(if (limit < 0) m else m min limit) max 20 |
|
23 |
} |
|
24 |
||
25 |
def component_margin(metric: Font_Metric, component: JComponent): Int = |
|
26 |
make_margin(metric, (component.getWidth.toDouble / metric.average_width).toInt) |
|
27 |
||
28 |
||
29 |
/* format */ |
|
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 | 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 | 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 | 48 |
Exn.Interrupt.expose() |
49 |
} |
|
50 |
result.toList |
|
51 |
} |
|
81428 | 52 |
|
53 |
def formatted_lines(formatted: List[Formatted]): Int = |
|
54 |
if (formatted.isEmpty) 0 |
|
55 |
else { |
|
56 |
1 + formatted.iterator.map(form => |
|
57 |
XML.traverse_text(form.body, 0, (n, s) => n + Library.count_newlines(s))).sum |
|
58 |
} |
|
59 |
||
60 |
def formatted_margin(metric: Font_Metric, formatted: List[Formatted]): Double = |
|
61 |
split_lines(formatted.map(_.text).mkString) |
|
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 | 103 |
} |