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	import ../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
11	type 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
15	def 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
24	def 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
32	def 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
40	def 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
44	def 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
53	def 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)