tuned;
authorwenzelm
Fri, 31 Oct 2025 11:31:36 +0100
changeset 83432 6b2db426f1b3
parent 83431 b41b4fa1ac6f
child 83433 e26f102d2498
tuned;
src/Tools/VSCode/src/lsp.scala
src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/lsp.scala	Wed Oct 29 22:07:05 2025 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Fri Oct 31 11:31:36 2025 +0100
@@ -593,8 +593,7 @@
         case Notification("PIDE/caret_update", Some(params)) =>
           val caret =
             for {
-              uri <- JSON.string(params, "uri")
-              if Url.is_wellformed_file(uri)
+              uri <- JSON.string(params, "uri") if Url.is_wellformed_file(uri)
               pos <- Position.unapply(params)
             } yield (Url.absolute_file(uri), pos)
           Some(caret)
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Oct 29 22:07:05 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Oct 31 11:31:36 2025 +0100
@@ -58,7 +58,7 @@
   private val dotted_elements =
     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING)
 
-  val tooltip_elements =
+  val tooltip_elements: Markup.Elements =
     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.BAD) ++
     Rendering.tooltip_elements