# HG changeset patch
# User wenzelm
# Date 1761906696 -3600
# Node ID 6b2db426f1b36d139f7d078958eb6b0a270cc540
# Parent  b41b4fa1ac6f020743ec02d22b59e4ab3cceb019
tuned;

diff -r b41b4fa1ac6f -r 6b2db426f1b3 src/Tools/VSCode/src/lsp.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)
diff -r b41b4fa1ac6f -r 6b2db426f1b3 src/Tools/VSCode/src/vscode_rendering.scala
--- 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