--- a/src/Pure/PIDE/protocol.scala Wed Oct 29 15:18:04 2025 +0100
+++ b/src/Pure/PIDE/protocol.scala Wed Oct 29 17:42:25 2025 +0100
@@ -254,7 +254,7 @@
/* sendback snippets */
- def senback_snippets(xml: XML.Body): List[(String, Properties.T)] = {
+ def sendback_snippets(xml: XML.Body): List[(String, Properties.T)] = {
var seen = Set.empty[(String, Properties.T)]
val result = new mutable.ListBuffer[(String, Properties.T)]
--- a/src/Tools/VSCode/src/language_server.scala Wed Oct 29 15:18:04 2025 +0100
+++ b/src/Tools/VSCode/src/language_server.scala Wed Oct 29 17:42:25 2025 +0100
@@ -428,32 +428,30 @@
text_range <- doc.text_range(range)
} {
val snapshot = resources.snapshot(model)
- val actions = snapshot
- .select(
- Text.Range(text_range.start - 1, text_range.stop + 1),
- Markup.Elements.full,
- command_states => _ => Some(command_states.flatMap(_.results.iterator.map(_._2).toList)))
- .flatMap(info => Protocol.senback_snippets(info.info).flatMap {
- (snippet, props) =>
- for {
- id <- Position.Id.unapply(props)
- (node, command) <- snapshot.find_command(id)
- start <- node.command_start(command)
- range = command.core_range + start
- current_text <- model.get_text(range)
- } yield {
- val line_range = doc.range(range)
- val edit_text =
- if (props.contains(Markup.PADDING_COMMAND)) {
- val whole_line = doc.lines(line_range.start.line)
- val indent = whole_line.text.takeWhile(_.isWhitespace)
- current_text + "\n" + Library.prefix_lines(indent, snippet)
- }
- else current_text + snippet
- val edit = LSP.TextEdit(line_range, resources.output_edit(edit_text))
- LSP.CodeAction(snippet, List(LSP.TextDocumentEdit(file, Some(version), List(edit))))
- }
- })
+ val results =
+ snapshot.command_results(Text.Range(text_range.start - 1, text_range.stop + 1))
+ .iterator.map(_._2).toList
+ val actions =
+ List.from(
+ for {
+ (snippet, props) <- Protocol.sendback_snippets(results).iterator
+ id <- Position.Id.unapply(props)
+ (node, command) <- snapshot.find_command(id)
+ start <- node.command_start(command)
+ range = command.core_range + start
+ current_text <- model.get_text(range)
+ } yield {
+ val line_range = doc.range(range)
+ val edit_text =
+ if (props.contains(Markup.PADDING_COMMAND)) {
+ val whole_line = doc.lines(line_range.start.line)
+ val indent = whole_line.text.takeWhile(_.isWhitespace)
+ current_text + "\n" + Library.prefix_lines(indent, snippet)
+ }
+ else current_text + snippet
+ val edit = LSP.TextEdit(line_range, resources.output_edit(edit_text))
+ LSP.CodeAction(snippet, List(LSP.TextDocumentEdit(file, Some(version), List(edit))))
+ })
channel.write(LSP.CodeActionRequest.reply(id, actions))
}
}