src/lsp/docs.bend
bolt@1.26.0.0 · 59 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.26.0.0/src/lazy/lazy.bend as Lazy
6import bolt@1.26.0.0/src/lsp/report.bend as Rep
7import bolt@1.26.0.0/src/role.bend as Role
8
9# an open document: its URI, the text the editor shows, the checker's errors
10# from its last run, and the role marks read with them
11type Doc is Data:
12 Doc{uri: String, text: String, errors: List<&2, Rep.Diag>, marks: List<&2, Role.Mark>}
13
14# the documents without the one at a URI
15def del(docs: List<&2, Doc>, +uri: String) -> List<&2, Doc>:
16 match docs:
17 case Nil{}:
18 Nil{}
19 case Con{Doc{+u, t, e, m}, r}:
20 +rest = del(r, uri)
21 Bool.pick(List<&2, Doc>, String.eq(u, uri), rest, Doc{u, t, e, m} <> rest)
22
23# the checker's errors for a document, none when it is not open
24def errors(docs: List<&2, Doc>, +uri: String) -> List<&2, Rep.Diag>:
25 match docs:
26 case Nil{}:
27 Nil{}
28 case Con{Doc{u, t, e, m}, r}:
29 Lazy.stop(List<&2, Rep.Diag>, String.eq(u, uri), e, _u => errors(r, uri))
30
31# the role marks kept for a document, none when it is not open
32def marks(docs: List<&2, Doc>, +uri: String) -> List<&2, Role.Mark>:
33 match docs:
34 case Nil{}:
35 Nil{}
36 case Con{Doc{u, t, e, m}, r}:
37 Lazy.stop(List<&2, Role.Mark>, String.eq(u, uri), m, _u => marks(r, uri))
38
39# a document's text set (opened, or changed); its errors and marks stay
40def set(+docs: List<&2, Doc>, +uri: String, text: String) -> List<&2, Doc>:
41 Doc{uri, text, errors(docs, uri), marks(docs, uri)} <> del(docs, uri)
42
43# the text of an open document, when it is open
44def get(docs: List<&2, Doc>, +uri: String) -> Maybe<&2, String>:
45 match docs:
46 case Nil{}:
47 None{}
48 case Con{Doc{u, t, e, m}, r}:
49 Lazy.stop(Maybe<&2, String>, String.eq(u, uri), Some{t}, _u => get(r, uri))
50
51# a document's errors set, from a run of the checker, with the marks read
52# beside it
53def set_checked(
54 +docs: List<&2, Doc>,
55 +uri: String,
56 errors: List<&2, Rep.Diag>,
57 ms: List<&2, Role.Mark>
58) -> List<&2, Doc>:
59 Doc{uri, Maybe.default(&2, String, get(docs, uri), ""), errors, ms} <> del(docs, uri)