clarified signature: more uniform ts vs. Scala;

--- 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 */

--- 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",

--- 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)