1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
|
(* The Sol language server: JSON-RPC over stdio, hand rolled on
yojson. One capability, the load-bearing one: diagnostics. Every
edit runs the same admission the runtime runs, so a rule with no
decrease witness or a fact violating its schema is an error in
the editor, at typing time, with the same message the loader
gives. Parse errors carry positions; admission errors anchor at
the top of the file until the loader learns locations. *)
let log_json json = Yojson.Safe.to_string json
let send json =
let body = log_json json in
Printf.printf "Content-Length: %d\r\n\r\n%s" (String.length body) body;
flush stdout
let read_message () =
let rec headers length =
match In_channel.input_line stdin with
| None -> None
| Some line -> (
let line = String.trim line in
if line = "" then length
else
match String.index_opt line ':' with
| Some i
when String.lowercase_ascii (String.sub line 0 i) = "content-length"
->
headers
(int_of_string_opt
(String.trim
(String.sub line (i + 1) (String.length line - i - 1))))
| _ -> headers length)
in
match headers None with
| None -> None
| Some length -> (
match really_input_string stdin length with
| body -> ( try Some (Yojson.Safe.from_string body) with _ -> None)
| exception End_of_file -> None)
let member name json =
match json with
| `Assoc fields -> Option.value ~default:`Null (List.assoc_opt name fields)
| _ -> `Null
let to_string_opt = function `String s -> Some s | _ -> None
(* Everything the checker can say about a document, as LSP
diagnostics: (line, column, message), zero-based lines. *)
let diagnostics text =
match Sol.Front.parse text with
| Error { Sol.Front.line; column; message } ->
[ (max 0 (line - 1), max 0 column, message) ]
| Ok statements -> (
match Sol.Program.load statements with
| Error error -> [ (0, 0, Format.asprintf "%a" Sol.Program.pp_error error) ]
| Ok _ -> [])
let publish uri text =
let items =
List.map
(fun (line, column, message) ->
`Assoc
[
( "range",
`Assoc
[
( "start",
`Assoc [ ("line", `Int line); ("character", `Int column) ]
);
( "end",
`Assoc
[ ("line", `Int line); ("character", `Int (column + 1)) ]
);
] );
("severity", `Int 1);
("source", `String "sol");
("message", `String message);
])
(diagnostics text)
in
send
(`Assoc
[
("jsonrpc", `String "2.0");
("method", `String "textDocument/publishDiagnostics");
("params", `Assoc [ ("uri", `String uri); ("diagnostics", `List items) ]);
])
let respond id result =
send (`Assoc [ ("jsonrpc", `String "2.0"); ("id", id); ("result", result) ])
let check_notification params =
let uri =
to_string_opt (member "uri" (member "textDocument" params))
in
let text =
match to_string_opt (member "text" (member "textDocument" params)) with
| Some text -> Some text
| None -> (
(* didChange, full sync: the last full content change. *)
match member "contentChanges" params with
| `List changes -> (
match List.rev changes with
| last :: _ -> to_string_opt (member "text" last)
| [] -> None)
| _ -> None)
in
match (uri, text) with Some uri, Some text -> publish uri text | _ -> ()
let run () =
set_binary_mode_in stdin true;
set_binary_mode_out stdout true;
let running = ref true in
while !running do
match read_message () with
| None -> running := false
| Some message -> (
let id = member "id" message in
let params = member "params" message in
match to_string_opt (member "method" message) with
| Some "initialize" ->
respond id
(`Assoc
[
( "capabilities",
`Assoc [ ("textDocumentSync", `Int 1) ] );
( "serverInfo",
`Assoc
[
("name", `String "sol-lsp"); ("version", `String "0.1.0");
] );
])
| Some "shutdown" -> respond id `Null
| Some "exit" -> running := false
| Some ("textDocument/didOpen" | "textDocument/didChange") ->
check_notification params
| Some "textDocument/didClose" -> (
match to_string_opt (member "uri" (member "textDocument" params)) with
| Some uri ->
send
(`Assoc
[
("jsonrpc", `String "2.0");
("method", `String "textDocument/publishDiagnostics");
( "params",
`Assoc
[ ("uri", `String uri); ("diagnostics", `List []) ] );
])
| None -> ())
| Some _ when id <> `Null ->
(* An unsupported request deserves an answer, not silence. *)
send
(`Assoc
[
("jsonrpc", `String "2.0");
("id", id);
( "error",
`Assoc
[
("code", `Int (-32601));
("message", `String "method not found");
] );
])
| _ -> ())
done
|
