author | wenzelm |
Mon, 25 Mar 2019 17:21:26 +0100 | |
changeset 69981 | 3dced198b9ec |
parent 66216 | d4949bae0bad |
child 75126 | da1108a6d249 |
permissions | -rw-r--r-- |
65201 | 1 |
'use strict'; |
2 |
||
3 |
import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions } from 'vscode' |
|
4 |
import { NotificationType } from 'vscode-languageclient'; |
|
66052
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65983
diff
changeset
|
5 |
import * as symbol from './symbol' |
65201 | 6 |
|
7 |
||
8 |
/* decorations */ |
|
9 |
||
10 |
export interface DecorationOpts { |
|
11 |
range: number[], |
|
12 |
hover_message?: MarkedString | MarkedString[] |
|
13 |
} |
|
14 |
||
15 |
export interface Decoration |
|
16 |
{ |
|
17 |
uri: string, |
|
18 |
"type": string, |
|
19 |
content: DecorationOpts[] |
|
20 |
} |
|
21 |
||
22 |
export const decoration_type = |
|
23 |
new NotificationType<Decoration, void>("PIDE/decoration") |
|
24 |
||
25 |
||
26 |
/* caret handling */ |
|
27 |
||
28 |
export interface Caret_Update |
|
29 |
{ |
|
30 |
uri?: string |
|
31 |
line?: number |
|
32 |
character?: number |
|
66216 | 33 |
focus?: boolean |
65201 | 34 |
} |
35 |
||
36 |
export const caret_update_type = |
|
37 |
new NotificationType<Caret_Update, void>("PIDE/caret_update") |
|
38 |
||
39 |
||
40 |
/* dynamic output */ |
|
41 |
||
42 |
export interface Dynamic_Output |
|
43 |
{ |
|
65979 | 44 |
content: string |
65201 | 45 |
} |
46 |
||
47 |
export const dynamic_output_type = |
|
48 |
new NotificationType<Dynamic_Output, void>("PIDE/dynamic_output") |
|
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65201
diff
changeset
|
49 |
|
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65201
diff
changeset
|
50 |
|
66096 | 51 |
/* state */ |
52 |
||
53 |
export interface State_Output |
|
54 |
{ |
|
55 |
id: number |
|
56 |
content: string |
|
57 |
} |
|
58 |
||
59 |
export const state_output_type = |
|
60 |
new NotificationType<State_Output, void>("PIDE/state_output") |
|
61 |
||
62 |
export interface State_Id |
|
63 |
{ |
|
64 |
id: number |
|
65 |
} |
|
66 |
||
66211 | 67 |
export interface Auto_Update |
68 |
{ |
|
69 |
id: number |
|
70 |
enabled: boolean |
|
71 |
} |
|
72 |
||
66096 | 73 |
export const state_init_type = new NotificationType<void, void>("PIDE/state_init") |
74 |
export const state_exit_type = new NotificationType<State_Id, void>("PIDE/state_exit") |
|
75 |
export const state_locate_type = new NotificationType<State_Id, void>("PIDE/state_locate") |
|
76 |
export const state_update_type = new NotificationType<State_Id, void>("PIDE/state_update") |
|
66211 | 77 |
export const state_auto_update_type = |
78 |
new NotificationType<Auto_Update, void>("PIDE/state_auto_update") |
|
66096 | 79 |
|
80 |
||
65983 | 81 |
/* preview */ |
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65201
diff
changeset
|
82 |
|
65983 | 83 |
export interface Preview_Request |
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65201
diff
changeset
|
84 |
{ |
65983 | 85 |
uri: string |
86 |
column: number |
|
87 |
} |
|
88 |
||
89 |
export interface Preview_Response |
|
90 |
{ |
|
91 |
uri: string |
|
92 |
column: number |
|
93 |
label: string |
|
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65201
diff
changeset
|
94 |
content: string |
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65201
diff
changeset
|
95 |
} |
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65201
diff
changeset
|
96 |
|
65983 | 97 |
export const preview_request_type = |
98 |
new NotificationType<Preview_Request, void>("PIDE/preview_request") |
|
99 |
||
100 |
export const preview_response_type = |
|
101 |
new NotificationType<Preview_Response, void>("PIDE/preview_response") |
|
66052
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65983
diff
changeset
|
102 |
|
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65983
diff
changeset
|
103 |
|
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65983
diff
changeset
|
104 |
/* Isabelle symbols */ |
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65983
diff
changeset
|
105 |
|
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65983
diff
changeset
|
106 |
export interface Symbols |
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65983
diff
changeset
|
107 |
{ |
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65983
diff
changeset
|
108 |
entries: [symbol.Entry] |
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65983
diff
changeset
|
109 |
} |
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65983
diff
changeset
|
110 |
|
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65983
diff
changeset
|
111 |
export const symbols_type = |
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65983
diff
changeset
|
112 |
new NotificationType<Symbols, void>("PIDE/symbols") |
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65983
diff
changeset
|
113 |
|
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65983
diff
changeset
|
114 |
export const symbols_request_type = |
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65983
diff
changeset
|
115 |
new NotificationType<void, void>("PIDE/symbols_request") |
66138 | 116 |
|
117 |
||
118 |
/* spell checker */ |
|
119 |
||
120 |
export const include_word_type = |
|
121 |
new NotificationType<void, void>("PIDE/include_word") |
|
122 |
||
123 |
export const include_word_permanently_type = |
|
124 |
new NotificationType<void, void>("PIDE/include_word_permanently") |
|
125 |
||
126 |
export const exclude_word_type = |
|
127 |
new NotificationType<void, void>("PIDE/exclude_word") |
|
128 |
||
129 |
export const exclude_word_permanently_type = |
|
130 |
new NotificationType<void, void>("PIDE/exclude_word_permanently") |
|
131 |
||
132 |
export const reset_words_type = |
|
133 |
new NotificationType<void, void>("PIDE/reset_words") |