--- a/src/Tools/VSCode/src/pretty_text_panel.scala Sun Jun 30 15:32:45 2024 +0200
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala Sun Jun 30 15:32:51 2024 +0200
@@ -75,7 +75,7 @@
.cumulate(Text.Range.full, None: Option[String], Rendering.text_color_elements, (_, m) => {
Some(Some(m.info.name))
})
- .flatMap(e => e._2 match {
+ .flatMap(e => e.info match {
case None => None
case Some(i) => Some((document.range(e._1), "text_" ++ Rendering.text_color(i).toString))
})
--- a/src/Tools/VSCode/src/vscode_rendering.scala Sun Jun 30 15:32:45 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Sun Jun 30 15:32:51 2024 +0200
@@ -79,7 +79,7 @@
def completion(node_pos: Line.Node_Position, caret: Text.Offset): List[LSP.CompletionItem] = {
val doc = model.content.doc
- val line = node_pos.pos.line
+ val line = node_pos.line
val unicode = resources.unicode_symbols_edits
doc.offset(Line.Position(line)) match {
case None => Nil