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).
4	import Base
5	import ../lazy/lazy.bend as Lazy
6	import ./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
10	type Doc is Data:
11	  Doc{uri: String, text: String, errors: List<&2, Rep.Diag>}
12	
13	# the documents without the one at a URI
14	def 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
23	def 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
31	def 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
35	def 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
43	def 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)