src/Tools/VSCode/extension/src/protocol.ts
author wenzelm
Sun, 12 Mar 2017 18:45:53 +0100
changeset 65201 2d01b30e6ac6
child 65977 c51b74be23b6
permissions -rw-r--r--
clarified modules;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65201
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
     1
'use strict';
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
     2
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
     3
import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions } from 'vscode'
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
     4
import { NotificationType } from 'vscode-languageclient';
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
     5
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
     6
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
     7
/* decorations */
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
     8
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
     9
export interface DecorationOpts {
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    10
  range: number[],
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    11
  hover_message?: MarkedString | MarkedString[]
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    12
}
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    13
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    14
export interface Decoration
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    15
{
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    16
  uri: string,
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    17
  "type": string,
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    18
  content: DecorationOpts[]
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    19
}
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    20
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    21
export const decoration_type =
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    22
  new NotificationType<Decoration, void>("PIDE/decoration")
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    23
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    24
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    25
/* caret handling */
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    26
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    27
export interface Caret_Update
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    28
{
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    29
  uri?: string
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    30
  line?: number
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    31
  character?: number
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    32
}
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    33
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    34
export const caret_update_type =
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    35
  new NotificationType<Caret_Update, void>("PIDE/caret_update")
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    36
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    37
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    38
/* dynamic output */
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    39
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    40
export interface Dynamic_Output
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    41
{
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    42
  body: string
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    43
}
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    44
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    45
export const dynamic_output_type =
2d01b30e6ac6 clarified modules;
wenzelm
parents:
diff changeset
    46
  new NotificationType<Dynamic_Output, void>("PIDE/dynamic_output")