# HG changeset patch
# User wenzelm
# Date 1731236136 -3600
# Node ID 206dd586f3d7cb36914aed47e2334b9af65aa668
# Parent  1e3dfb722ee6e2c0c5c94f0d5029062e85a9a63d
clarified modules;

diff -r 1e3dfb722ee6 -r 206dd586f3d7 etc/build.props
--- 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 \
diff -r 1e3dfb722ee6 -r 206dd586f3d7 src/Pure/GUI/rich_text.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)
+  }
+}
diff -r 1e3dfb722ee6 -r 206dd586f3d7 src/Tools/jEdit/src/pretty_text_area.scala
--- 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()
     }