src/lsp/docs.bend

bolt@1.11.0.0 · 44 lines · 0 definitions

1# lsp/docs: the open documents, by URI: what the editor shows, saved or not,
2# and the checker's last word on each (its errors come from the file on disk,
3# the linter's warnings from the text, so both are needed to publish).
4import Base
5import bolt@1.11.0.0/src/lazy/lazy.bend as Lazy
6import bolt@1.11.0.0/src/lsp/report.bend as Rep
7
8# an open document: its URI, the text the editor shows, the checker's errors
9# from its last run
10type Doc is Data:
11  Doc{uri: String, text: String, errors: List<&2, Rep.Diag>}
12
13# the documents without the one at a URI
14def del(docs: List<&2, Doc>, +uri: String) -> List<&2, Doc>:
15  match docs:
16    case Nil{}:
17      Nil{}
18    case Con{Doc{+u, t, e}, r}:
19      +rest = del(r, uri)
20      Bool.pick(List<&2, Doc>, String.eq(u, uri), rest, Doc{u, t, e} <> rest)
21
22# the checker's errors for a document, none when it is not open
23def errors(docs: List<&2, Doc>, +uri: String) -> List<&2, Rep.Diag>:
24  match docs:
25    case Nil{}:
26      Nil{}
27    case Con{Doc{u, t, e}, r}:
28      Lazy.stop(List<&2, Rep.Diag>, String.eq(u, uri), e, _u => errors(r, uri))
29
30# a document's text set (opened, or changed); its errors stay
31def set(+docs: List<&2, Doc>, +uri: String, text: String) -> List<&2, Doc>:
32  Doc{uri, text, errors(docs, uri)} <> del(docs, uri)
33
34# the text of an open document, when it is open
35def get(docs: List<&2, Doc>, +uri: String) -> Maybe<&2, String>:
36  match docs:
37    case Nil{}:
38      None{}
39    case Con{Doc{u, t, e}, r}:
40      Lazy.stop(Maybe<&2, String>, String.eq(u, uri), Some{t}, _u => get(r, uri))
41
42# a document's errors set, from a run of the checker
43def set_errors(+docs: List<&2, Doc>, +uri: String, errors: List<&2, Rep.Diag>) -> List<&2, Doc>:
44  Doc{uri, Maybe.default(&2, String, get(docs, uri), ""), errors} <> del(docs, uri)