Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[fleche] Document-structure support #322

Open
ejgallego opened this issue Feb 14, 2023 · 0 comments
Open

[fleche] Document-structure support #322

ejgallego opened this issue Feb 14, 2023 · 0 comments
Milestone
0.3.0

Comments

@ejgallego
Copy link
Owner

ejgallego commented Feb 14, 2023 •
edited
Loading

As of today, documents are flat, but we want to query the language manager for structure and reflect that in our model.

This is the continuation of #325

Related issues:
@ejgallego ejgallego added this to the 0.2.0 milestone Feb 14, 2023
@ejgallego ejgallego mentioned this issue Feb 14, 2023
Closed
@ejgallego ejgallego modified the milestones: 0.2.0, 0.1.7 Feb 16, 2023
ejgallego added a commit that referenced this issue Feb 16, 2023
@ejgallego
[doc] Refactor find_proof into ast finding + action
ac1edf2 
Until we implement #322 , this will help with #310
@ejgallego ejgallego mentioned this issue Feb 16, 2023
Merged
ejgallego added a commit that referenced this issue Feb 16, 2023
@ejgallego
[doc] Refactor find_proof into ast finding + action
a182580 
Until we implement #322 , this will help with #310
ejgallego added a commit that referenced this issue Feb 16, 2023
@ejgallego
[doc] Refactor find_proof into ast finding + action
c0f7d1b 
Until we implement #322 , this will help with #310
@ejgallego ejgallego modified the milestones: 0.2.0, 0.1.8 Jun 29, 2023
ejgallego added a commit that referenced this issue Sep 26, 2023
@ejgallego
[fleche] Support for structure in documents
ec35ab4 
Nodes can now have children; this gives the consumers (error recovery,
document outline, analysis tools, etc...) a much more convenient
representation of the document.

We postpone adapting the document outline code to a further PR, so we
have tested this with the `coq/getDocument` API call.

As it is sadly the case for most `coq-lsp` features, I don't have the
resources to add a test case, so tagging this with `needs: test-case`
for the future.

Fixes #322
ejgallego added a commit that referenced this issue Oct 2, 2023
@ejgallego
[fleche] Support for structure in documents
95d68f1 
Nodes can now have children; this gives the consumers (error recovery,
document outline, analysis tools, etc...) a much more convenient
representation of the document.

We postpone adapting the document outline code to a further PR, so we
have tested this with the `coq/getDocument` API call.

As it is sadly the case for most `coq-lsp` features, I don't have the
resources to add a test case, so tagging this with `needs: test-case`
for the future.

Fixes #322
@ejgallego ejgallego modified the milestones: 0.1.8, 0.1.9 Oct 25, 2023
@ejgallego ejgallego modified the milestones: 0.1.9, 0.1.10 Nov 8, 2023
@ejgallego ejgallego mentioned this issue May 15, 2024
Merged
@ejgallego ejgallego modified the milestones: 0.1.9.1, 0.2.0, 0.3.0 May 31, 2024
@ejgallego ejgallego mentioned this issue Dec 5, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
0.3.0
Development

No branches or pull requests
1 participant
@ejgallego