--- a/src/Pure/PIDE/command.scala Fri Nov 08 16:57:48 2024 +0100
+++ b/src/Pure/PIDE/command.scala Fri Nov 08 18:34:33 2024 +0100
@@ -388,8 +388,8 @@
def text(source: String): Command = unparsed(source)
- def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command =
- unparsed(XML.content(body), id = id, results = results,
+ def rich_text(body: XML.Body = Nil, results: Results = Results.empty): Command =
+ unparsed(XML.content(body), id = Document_ID.make(), results = results,
markups = Markups.init(Markup_Tree.from_XML(body)))
--- a/src/Tools/jEdit/src/jedit_rendering.scala Fri Nov 08 16:57:48 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Fri Nov 08 18:34:33 2024 +0100
@@ -25,16 +25,10 @@
def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering =
new JEdit_Rendering(snapshot, model, options)
- def text(
- snapshot: Document.Snapshot,
- formatted_body: XML.Body,
- results: Command.Results = Command.Results.empty
- ): (String, JEdit_Rendering) = {
- val command = Command.rich_text(Document_ID.make(), results, formatted_body)
- val snippet = snapshot.snippet(command, Document.Blobs.empty)
+ def apply(snapshot: Document.Snapshot, rich_text: Command): JEdit_Rendering = {
+ val snippet = snapshot.snippet(rich_text, Document.Blobs.empty)
val model = File_Model.init(PIDE.session)
- val rendering = apply(snippet, model, PIDE.options.value)
- (command.source, rendering)
+ apply(snippet, model, PIDE.options.value)
}
--- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Nov 08 16:57:48 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Nov 08 18:34:33 2024 +0100
@@ -41,7 +41,7 @@
private var current_base_snapshot = Document.Snapshot.init
private var current_base_results = Command.Results.empty
private var current_rendering: JEdit_Rendering =
- JEdit_Rendering.text(current_base_snapshot, Nil)._2
+ JEdit_Rendering(current_base_snapshot, Command.rich_text())
private var future_refresh: Option[Future[Unit]] = None
private val rich_text_area =
@@ -99,7 +99,10 @@
future_refresh =
Some(Future.fork {
val (text, rendering) =
- try { JEdit_Rendering.text(snapshot, formatted, results = results) }
+ try {
+ val rich_text = Command.rich_text(body = formatted, results = results)
+ (rich_text.source, JEdit_Rendering(snapshot, rich_text))
+ }
catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
Exn.Interrupt.expose()