# HG changeset patch # User wenzelm # Date 1731184478 -3600 # Node ID ed4ff84e9b2177b921de950d6cb63f3439887dfa # Parent 2d9b6e32632ddbba17a53aac0a1c46e000ac3c8b Document.Snapshot: support for multiple snippet_commands; clarified Command.rich_text: prefer explicit id, e.g. from message serial; clarified Pretty_Text_Area.update: Protocol_Message.provide_serial; clarified Pretty_Text_Area.format_rich_texts, with separate formatting of messages; diff -r 2d9b6e32632d -r ed4ff84e9b21 src/Pure/Build/build.scala --- a/src/Pure/Build/build.scala Sat Nov 09 16:39:33 2024 +0100 +++ b/src/Pure/Build/build.scala Sat Nov 09 21:34:38 2024 +0100 @@ -764,7 +764,7 @@ val doc_blobs = Document.Blobs.make(blobs) - Document.State.init.snippet(command, doc_blobs) + Document.State.init.snippet(List(command), doc_blobs) } } diff -r 2d9b6e32632d -r ed4ff84e9b21 src/Pure/Build/build_job.scala --- a/src/Pure/Build/build_job.scala Sat Nov 09 16:39:33 2024 +0100 +++ b/src/Pure/Build/build_job.scala Sat Nov 09 21:34:38 2024 +0100 @@ -300,7 +300,7 @@ def export_text(name: String, text: String, compress: Boolean = true): Unit = export_(name, List(XML.Text(text)), compress = compress) - for (command <- snapshot.snippet_command) { + for (command <- snapshot.snippet_commands) { export_text(Export.DOCUMENT_ID, command.id.toString, compress = false) } diff -r 2d9b6e32632d -r ed4ff84e9b21 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Sat Nov 09 16:39:33 2024 +0100 +++ b/src/Pure/PIDE/command.scala Sat Nov 09 21:34:38 2024 +0100 @@ -386,9 +386,17 @@ new Command(id, node_name, blobs_info, span1, source1, results, markups) } - def rich_text(body: XML.Body = Nil, results: Results = Results.empty): Command = - unparsed(XML.content(body), id = Document_ID.make(), results = results, + def rich_text( + body: XML.Body = Nil, + id: Document_ID.Command = Document_ID.none, + results: Results = Results.empty + ): Command = { + unparsed(XML.content(body), id = id, results = results, markups = Markups.init(Markup_Tree.from_XML(body))) + } + + def full_source(commands: Iterable[Command]): String = + commands.iterator.map(_.source).mkString /* edits and perspective */ diff -r 2d9b6e32632d -r ed4ff84e9b21 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat Nov 09 16:39:33 2024 +0100 +++ b/src/Pure/PIDE/document.scala Sat Nov 09 21:34:38 2024 +0100 @@ -568,7 +568,7 @@ val version: Version, val node_name: Node.Name, pending_edits: Pending_Edits, - val snippet_command: Option[Command] + val snippet_commands: List[Command] ) { override def toString: String = "Snapshot(node = " + node_name.node + ", version = " + version.id + @@ -576,7 +576,7 @@ def switch(name: Node.Name): Snapshot = if (name == node_name) this - else new Snapshot(state, version, name, pending_edits, None) + else new Snapshot(state, version, name, pending_edits, Nil) /* nodes */ @@ -628,27 +628,41 @@ /* command as add-on snippet */ - def snippet(command: Command, doc_blobs: Blobs): Snapshot = { - val node_name = command.node_name + def snippet(commands: List[Command], doc_blobs: Blobs): Snapshot = { + require(commands.nonEmpty, "no snippet commands") + + val node_name = commands.head.node_name + val node_commands = Linear_Set.from(commands) - val blobs = for (a <- command.blobs_names; b <- doc_blobs.get(a)) yield a -> b + require(commands.forall(command => command.node_name == node_name), + "incoherent snippet node names") + + val blobs = + for { + command <- commands + a <- command.blobs_names + b <- doc_blobs.get(a) + } yield a -> b val nodes0 = version.nodes - val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command))) + val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(node_commands)) val nodes2 = blobs.foldLeft(nodes1) { case (ns, (a, b)) => ns + (a -> Node.init_blob(b)) } val version1 = Version.make(nodes2) val edits: List[Edit_Text] = - List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source)))) ::: + List(node_name -> Node.Edits(List(Text.Edit.insert(0, Command.full_source(commands))))) ::: blobs.map({ case (a, b) => a -> Node.Blob(b) }) - val state0 = state.define_command(command) + val assign_update: Assign_Update = + commands.map(command => command.id -> List(Document_ID.make())) + + val state0 = commands.foldLeft(state)(_.define_command(_)) val state1 = state0.continue_history(Future.value(version), edits, Future.value(version1)) .define_version(version1, state0.the_assignment(version)) - .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2 + .assign(version1.id, Nil, assign_update)._2 - state1.snapshot(node_name = node_name, snippet_command = Some(command)) + state1.snapshot(node_name = node_name, snippet_commands = commands) } @@ -1030,7 +1044,7 @@ Command.unparsed(command.source, theory = true, id = id, node_name = node_name, blobs_info = command.blobs_info, results = st.results, markups = st.markups) val state1 = copy(theories = theories - id) - (state1.snippet(command1, doc_blobs), state1) + (state1.snippet(List(command1), doc_blobs), state1) } def assign( @@ -1254,7 +1268,7 @@ def snapshot( node_name: Node.Name = Node.Name.empty, pending_edits: Pending_Edits = Pending_Edits.empty, - snippet_command: Option[Command] = None + snippet_commands: List[Command] = Nil ): Snapshot = { val stable = recent_stable val version = stable.version.get_finished @@ -1265,10 +1279,10 @@ case (name, Node.Edits(es)) <- change.rev_edits } yield (name -> es)).foldLeft(pending_edits)(_ + _) - new Snapshot(this, version, node_name, pending_edits1, snippet_command) + new Snapshot(this, version, node_name, pending_edits1, snippet_commands) } - def snippet(command: Command, doc_blobs: Blobs): Snapshot = - snapshot().snippet(command, doc_blobs) + def snippet(commands: List[Command], doc_blobs: Blobs): Snapshot = + snapshot().snippet(commands, doc_blobs) } } diff -r 2d9b6e32632d -r ed4ff84e9b21 src/Pure/PIDE/protocol_message.scala --- a/src/Pure/PIDE/protocol_message.scala Sat Nov 09 16:39:33 2024 +0100 +++ b/src/Pure/PIDE/protocol_message.scala Sat Nov 09 21:34:38 2024 +0100 @@ -34,6 +34,13 @@ } + /* message serial */ + + def provide_serial(msg: XML.Elem): XML.Elem = + if (Markup.Serial.get(msg.markup.properties) != 0L) msg + else msg.copy(markup = msg.markup.update_properties(Markup.Serial(Document_ID.make()))) + + /* inlined reports */ val report_elements: Markup.Elements = Markup.Elements(Markup.REPORT) diff -r 2d9b6e32632d -r ed4ff84e9b21 src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Sat Nov 09 16:39:33 2024 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Sat Nov 09 21:34:38 2024 +0100 @@ -25,10 +25,12 @@ def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering = new JEdit_Rendering(snapshot, model, options) - def apply(snapshot: Document.Snapshot, rich_text: Command): JEdit_Rendering = { - val snippet = snapshot.snippet(rich_text, Document.Blobs.empty) + def apply(snapshot: Document.Snapshot, rich_texts: List[Command]): JEdit_Rendering = { + val snapshot1 = + if (rich_texts.isEmpty) snapshot + else snapshot.snippet(rich_texts, Document.Blobs.empty) val model = File_Model.init(PIDE.session) - apply(snippet, model, PIDE.options.value) + apply(snapshot1, model, PIDE.options.value) } diff -r 2d9b6e32632d -r ed4ff84e9b21 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Sat Nov 09 16:39:33 2024 +0100 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Sat Nov 09 21:34:38 2024 +0100 @@ -18,6 +18,7 @@ import scala.swing.{Label, Component} import scala.util.matching.Regex +import scala.collection.mutable import org.gjt.sp.jedit.{jEdit, View, Registers, JEditBeanShellAction} import org.gjt.sp.jedit.input.{DefaultInputHandlerProvider, TextAreaInputHandler} @@ -27,6 +28,24 @@ import org.gjt.sp.util.{SyntaxUtilities, Log} +object Pretty_Text_Area { + def format_rich_texts( + output: List[XML.Elem], + metric: Font_Metric, + results: Command.Results + ): List[Command] = { + val result = new mutable.ListBuffer[Command] + for (msg <- output) { + if (result.nonEmpty) { + result += Command.rich_text(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.toList + } +} + class Pretty_Text_Area( view: View, close_action: () => Unit = () => (), @@ -40,8 +59,7 @@ private var current_output: List[XML.Elem] = Nil private var current_base_snapshot = Document.Snapshot.init private var current_base_results = Command.Results.empty - private var current_rendering: JEdit_Rendering = - JEdit_Rendering(current_base_snapshot, Command.rich_text()) + private var current_rendering: JEdit_Rendering = JEdit_Rendering(current_base_snapshot, Nil) private var future_refresh: Option[Future[Unit]] = None private val rich_text_area = @@ -95,11 +113,12 @@ future_refresh.foreach(_.cancel()) future_refresh = Some(Future.fork { - val formatted = - Pretty.formatted(Pretty.separate(output), margin = metric.margin, metric = metric) - val rich_text = Command.rich_text(body = formatted, results = results) - val rendering = - try { JEdit_Rendering(snapshot, rich_text) } + val (text, rendering) = + try { + val rich_texts = Pretty_Text_Area.format_rich_texts(output, metric, results) + val rendering = JEdit_Rendering(snapshot, rich_texts) + (Command.full_source(rich_texts), rendering) + } catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn } Exn.Interrupt.expose() @@ -113,7 +132,7 @@ JEdit_Lib.buffer_edit(getBuffer) { rich_text_area.active_reset() getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering)) - JEdit_Lib.buffer_undo_in_progress(getBuffer, setText(rich_text.source)) + JEdit_Lib.buffer_undo_in_progress(getBuffer, setText(text)) setCaretPosition(0) } } @@ -137,7 +156,7 @@ current_base_snapshot = base_snapshot current_base_results = base_results - current_output = output + current_output = output.map(Protocol_Message.provide_serial) refresh() }