--- a/etc/build.props Sun Nov 10 11:38:23 2024 +0100
+++ b/etc/build.props Sun Nov 10 11:55:36 2024 +0100
@@ -82,6 +82,7 @@
src/Pure/GUI/gui.scala \
src/Pure/GUI/gui_thread.scala \
src/Pure/GUI/popup.scala \
+ src/Pure/GUI/rich_text.scala \
src/Pure/GUI/tree_view.scala \
src/Pure/GUI/wrap_panel.scala \
src/Pure/General/antiquote.scala \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/GUI/rich_text.scala Sun Nov 10 11:55:36 2024 +0100
@@ -0,0 +1,20 @@
+/* Title: Pure/GUI/rich_text.scala
+ Author: Makarius
+
+Support for rendering of rich text, based on individual messages (XML.Elem).
+*/
+
+package isabelle
+
+
+object Rich_Text {
+ def command(
+ body: XML.Body = Nil,
+ id: Document_ID.Command = Document_ID.none,
+ results: Command.Results = Command.Results.empty
+ ): Command = {
+ val source = XML.content(body)
+ val markups = Command.Markups.init(Markup_Tree.from_XML(body))
+ Command.unparsed(source, id = id, results = results, markups = markups)
+ }
+}
--- a/src/Tools/jEdit/src/pretty_text_area.scala Sun Nov 10 11:38:23 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Sun Nov 10 11:55:36 2024 +0100
@@ -37,10 +37,10 @@
val result = new mutable.ListBuffer[Command]
for (msg <- output) {
if (result.nonEmpty) {
- result += Command.rich_text(body = Pretty.Separator, id = Document_ID.make())
+ result += Rich_Text.command(body = Pretty.Separator, id = Document_ID.make())
}
val body = Pretty.formatted(List(msg), margin = metric.margin, metric = metric)
- result += Command.rich_text(body = body, id = Markup.Serial.get(msg.markup.properties))
+ result += Rich_Text.command(body = body, id = Markup.Serial.get(msg.markup.properties))
Exn.Interrupt.expose()
}