# HG changeset patch
# User wenzelm
# Date 1489158440 -3600
# Node ID 3700be571a01d902080aa98c5a4e34a1b7850a28
# Parent  365e97f009ed905c480496775a6f7d07525903a0
more compact protocol message;

diff -r 365e97f009ed -r 3700be571a01 src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Fri Mar 10 14:16:45 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Fri Mar 10 16:07:20 2017 +0100
@@ -1,7 +1,7 @@
 'use strict';
 
 import * as vscode from 'vscode'
-import { Range, MarkedString, DecorationOptions, DecorationRenderOptions,
+import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions,
   TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
 
 
@@ -114,11 +114,16 @@
 
 /* decoration for document node */
 
+interface DecorationOpts {
+  range: number[],
+  hover_message?: MarkedString | MarkedString[]
+}
+
 export interface Decoration
 {
   uri: string,
   "type": string,
-  content: DecorationOptions[]
+  content: DecorationOpts[]
 }
 
 type Content = Range[] | DecorationOptions[]
@@ -129,24 +134,27 @@
   document_decorations.delete(document.uri.toString())
 }
 
-export function apply_decoration(decoration0: Decoration)
+export function apply_decoration(decoration: Decoration)
 {
-  const typ = types[decoration0.type]
+  const typ = types[decoration.type]
   if (typ) {
-    const decoration =
-    {
-      uri: Uri.parse(decoration0.uri).toString(),
-      "type": decoration0.type,
-      content: decoration0.content
-    }
+    const uri = Uri.parse(decoration.uri).toString()
+    const content: DecorationOptions[] = decoration.content.map(opt =>
+      {
+        const r = opt.range
+        return {
+          range: new Range(new Position(r[0], r[1]), new Position(r[2], r[3])),
+          hoverMessage: opt.hover_message
+        }
+      })
 
-    const document = document_decorations.get(decoration.uri) || new Map<string, Content>()
-    document.set(decoration.type, decoration.content)
-    document_decorations.set(decoration.uri, document)
+    const document = document_decorations.get(uri) || new Map<string, Content>()
+    document.set(decoration.type, content)
+    document_decorations.set(uri, document)
 
     for (const editor of vscode.window.visibleTextEditors) {
-      if (decoration.uri === editor.document.uri.toString()) {
-        editor.setDecorations(typ, decoration.content)
+      if (uri === editor.document.uri.toString()) {
+        editor.setDecorations(typ, content)
       }
     }
   }
diff -r 365e97f009ed -r 3700be571a01 src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Fri Mar 10 14:16:45 2017 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Fri Mar 10 16:07:20 2017 +0100
@@ -169,6 +169,9 @@
 
   object Range
   {
+    def compact(range: Line.Range): List[Int] =
+      List(range.start.line, range.start.column, range.stop.line, range.stop.column)
+
     def apply(range: Line.Range): JSON.T =
       Map("start" -> Position(range.start), "end" -> Position(range.stop))
 
@@ -404,21 +407,17 @@
 
   /* decorations */
 
-  sealed case class DecorationOptions(range: Line.Range, hover_message: List[MarkedString])
+  sealed case class DecorationOpts(range: Line.Range, hover_message: List[MarkedString])
   {
-    def no_hover_message: Boolean = hover_message.isEmpty
-    def json_range: JSON.T = Range(range)
     def json: JSON.T =
-      Map("range" -> json_range) ++
-      JSON.optional("hoverMessage" -> MarkedStrings.json(hover_message))
+      Map("range" -> Range.compact(range)) ++
+      JSON.optional("hover_message" -> MarkedStrings.json(hover_message))
   }
 
-  sealed case class Decoration(typ: String, content: List[DecorationOptions])
+  sealed case class Decoration(typ: String, content: List[DecorationOpts])
   {
-    def json_content: JSON.T =
-      if (content.forall(_.no_hover_message)) content.map(_.json_range) else content.map(_.json)
     def json(file: JFile): JSON.T =
       Notification("PIDE/decoration",
-        Map("uri" -> Url.print_file(file), "type" -> typ, "content" -> json_content))
+        Map("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json)))
   }
 }
diff -r 365e97f009ed -r 3700be571a01 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 10 14:16:45 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 10 16:07:20 2017 +0100
@@ -162,7 +162,7 @@
       for (Text.Info(text_range, msgs) <- decoration.content)
       yield {
         val range = model.content.doc.range(text_range)
-        Protocol.DecorationOptions(range,
+        Protocol.DecorationOpts(range,
           msgs.map(msg => Protocol.MarkedString(resources.output_pretty_tooltip(msg))))
       }
     Protocol.Decoration(decoration.typ, content)