# HG changeset patch
# User wenzelm
# Date 1647000426 -3600
# Node ID 0a440e255a64a4644d7fa1cccf9e5bdf812e65b2
# Parent  ec62c54015225b11350861d5ba61af54865d7ba9
clarified signature: more uniform ts vs. Scala;

diff -r ec62c5401522 -r 0a440e255a64 src/Tools/VSCode/extension/src/lsp.ts
--- a/src/Tools/VSCode/extension/src/lsp.ts	Fri Mar 11 12:56:37 2022 +0100
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Fri Mar 11 13:07:06 2022 +0100
@@ -8,7 +8,6 @@
 
 import { MarkdownString } from 'vscode'
 import { NotificationType } from 'vscode-languageclient'
-import * as symbol from './symbol'
 
 
 /* decorations */
diff -r ec62c5401522 -r 0a440e255a64 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Fri Mar 11 12:56:37 2022 +0100
+++ b/src/Tools/VSCode/src/lsp.scala	Fri Mar 11 13:07:06 2022 +0100
@@ -503,14 +503,14 @@
 
   /* decorations */
 
-  sealed case class DecorationOpts(range: Line.Range, hover_message: List[MarkedString])
+  sealed case class Decoration_Options(range: Line.Range, hover_message: List[MarkedString])
   {
     def json: JSON.T =
       JSON.Object("range" -> Range.compact(range)) ++
       JSON.optional("hover_message" -> MarkedStrings.json(hover_message))
   }
 
-  sealed case class Decoration(decorations: List[(String, List[DecorationOpts])])
+  sealed case class Decoration(decorations: List[(String, List[Decoration_Options])])
   {
     def json(file: JFile): JSON.T =
       Notification("PIDE/decoration",
diff -r ec62c5401522 -r 0a440e255a64 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 11 12:56:37 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 11 13:07:06 2022 +0100
@@ -243,7 +243,7 @@
         val decopts = for(Text.Info(text_range, msgs) <- deco.content)
           yield {
             val range = model.content.doc.range(text_range)
-            LSP.DecorationOpts(range,
+            LSP.Decoration_Options(range,
               msgs.map(msg => LSP.MarkedString(resources.output_pretty_tooltip(msg))))
           }
         (deco.typ, decopts)