feat: textDocument/foldingRange

[KacperFKorban]

closes #799 #137

[shilangyu]

💌

[shilangyu]

How will this work if we really are in the middle of parsing? The client won't ask us again for the folding ranges once we are done parsing, no?

[KacperFKorban]

You're right. I pretty much copy-pasted the code from other requests that require parsing. Maybe we should implement some callback mechanism for those, so that the requests would resume after parsing is done...

[gares]

I don't know about folding ranges, but for the overview we do return the message "not ready yet" but vscode never asks again. It seems a bug in vscode (or better, it does not implement LSP as designed).

[KacperFKorban]

Hmmm, IIUC the ServerCancelled error is only supported for semantic tokens and diagnostics.

[shilangyu]

Should parsing be an asynchronous task then? It seems reasonable to me for the LSP to wait until it is done with parsing before responding to a request.

[KacperFKorban]

That seems reasonable. Still, I would implement that in a new PR, and allow for returning ServerCancelled here for now.

[gares]

Can you have a look at the outline? (it is roughly a bunch of ranges with a label)

There is quite some code that is common, in spirit at least.

vsrocq/language-server/dm/document.ml

Lines 191 to 252 in 90a46b4

	let record_outline document id (ast : Synterp.vernac_control_entry) classif (outline : outline_element list) =
	let open Vernacextend in
	match classif with
	| VtProofStep _ | VtQed _ -> push_proof_step_in_outline document id outline
	| VtStartProof (_, names) ->
	let vernac_gen_expr = ast.v.expr in
	let type_ = match vernac_gen_expr with
	| VernacSynterp _ -> None
	| VernacSynPure pure ->
	match pure with
	| Vernacexpr.VernacStartTheoremProof _ -> Some TheoremKind
	| Vernacexpr.VernacDefinition _ -> Some DefinitionType
	| Vernacexpr.VernacFixpoint _ -> Some DefinitionType
	| Vernacexpr.VernacCoFixpoint _ -> Some DefinitionType
	| _ -> None
	in
	let str_names =
	match names with
	| [] -> ["default"]
	| _ -> List.map (fun n -> Names.Id.to_string n) names
	in
	begin match type_ with
	| None -> outline
	| Some type_ ->
	let range = range_of_id document id in
	let statement = string_of_id document id in
	let elements = List.map (fun name -> {id; type_; name; statement; range; proof=[]}) str_names in
	List.append elements outline
	end
	| VtSideff (names, _) ->
	let vernac_gen_expr = ast.v.expr in
	let type_, statement = match vernac_gen_expr with
	| VernacSynterp (Synterp.EVernacExtend _) when names <> [] -> Some Other, "external"
	| VernacSynterp (Synterp.EVernacBeginSection _) -> log (fun () -> Format.sprintf "BEGIN SECTION %s" (string_of_id document id)); Some BeginSection, ""
	| VernacSynterp (Synterp.EVernacDeclareModuleType _) -> log (fun () -> Format.sprintf "BEGIN MODULE %s" (string_of_id document id)); Some BeginModule, ""
	| VernacSynterp (Synterp.EVernacDefineModule _) -> log (fun () -> Format.sprintf "BEGIN MODULE %s" (string_of_id document id)); Some BeginModule, ""
	| VernacSynterp (Synterp.EVernacDeclareModule _) -> log (fun () -> Format.sprintf "BEGIN MODULE %s" (string_of_id document id)); Some BeginModule, ""
	| VernacSynterp (Synterp.EVernacEndSegment _) -> log (fun () -> Format.sprintf "END SEGMENT"); Some End, ""
	| VernacSynterp _ -> None, ""
	| VernacSynPure pure ->
	match pure with
	| Vernacexpr.VernacStartTheoremProof _ -> Some TheoremKind, string_of_id document id
	| Vernacexpr.VernacDefinition _ -> Some DefinitionType, string_of_id document id
	| Vernacexpr.VernacInductive _ -> Some InductiveType, string_of_id document id
	| Vernacexpr.VernacFixpoint _ -> Some DefinitionType, string_of_id document id
	| Vernacexpr.VernacCoFixpoint _ -> Some DefinitionType, string_of_id document id
	| _ -> None, ""
	in
	let str_names =
	match names with
	| [] -> ["default"]
	| _ -> List.map (fun n -> Names.Id.to_string n) names
	in
	begin match type_ with
	| None -> outline
	| Some type_ ->
	let range = range_of_id document id in
	let element = List.map (fun name -> {id; type_; name; statement; range; proof=[]}) str_names in
	List.append element outline
	end
	| _ -> outline

I wonder if it makes sense to have the outline be a projection of this folding info...

[KacperFKorban]

I designed the folding code with that in mind, I think that it should be fairly easy to reuse the new folding logic for the outline. I use a more "structured" type as an intermediate datatype that should also preserve the nesting information needed for the outline.
I think that we should be able to slightly extend this datatype and be able to project both the folding ranges and the outline from that. (One thing that would have to be filtered out is the indentation-based "fallback" ranges)

[KacperFKorban]

Do you prefer merging the two features in one PR or is it OK to do a separate one for refactoring the outline?

[gares]

If it is true that this new code is fast enough and a superset of the other, I think the best way to proceed is to:

1. add to the folding ranges data structure the "labels" used by the overview
2. write the projections
3. remove the old overview code and call the new one

Then we merge 1+2 in a PR. Finally we replace the overview code with 3.
If 3 turns out be not be ok, we can just revert one PR and still keep the folding.
But I think it is easier to develop 3 atop the other changes, and just (not) merge the last commit.