--- a/src/Tools/VSCode/extension/src/decorations.ts Sun Mar 12 18:05:06 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts Sun Mar 12 18:45:53 2017 +0100
@@ -4,6 +4,7 @@
import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions,
TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
import { get_color } from './extension'
+import { Decoration } from './protocol'
/* known decoration types */
@@ -133,18 +134,6 @@
/* decoration for document node */
-interface DecorationOpts {
- range: number[],
- hover_message?: MarkedString | MarkedString[]
-}
-
-export interface Decoration
-{
- uri: string,
- "type": string,
- content: DecorationOpts[]
-}
-
type Content = Range[] | DecorationOptions[]
const document_decorations = new Map<string, Map<string, Content>>()