src/lsp/docs.bend

bolt@1.27.0.0 · 59 lines · 7 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.27.0.0/src/lazy/lazy.bend as Lazy
6import bolt@1.27.0.0/src/lsp/report.bend as Rep
7import bolt@1.27.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)