# 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() }