Cancel parsing event #941
Merged
Cancel parsing event #941
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
rtetley
force-pushed
the
cancel-event
branch
from
4d7bc58 to
0f03284
Compare
|
This is a big one, still WIP. Needs:
|
In order to interupt a full document parse, we first need to make it part of the event loop.
rtetley
force-pushed
the
cancel-event
branch
from
ef1d45c to
305a024
Compare
We introduce parse events for each line which will allow for better interuptibility as well as laying the ground work for blocking on parse errors.
…parsing is over This brings back performance to acceptable levels.
- Removed some commented out dead code - Cleaned up ParseEvent (it doesnt need any info) - Cleaned up the api (removed unecessary variables to init, reset, etc...) - Removed cancel handle for ParseEvent
Now instead of launching execution directly from the lsp event, we queue a new event that has less priority then parsing.
The operations on range lists used to compute the overview could be re-used somewhere else
This will allow to easily recompute the overview from an invalidated state, and makes a correspondance between an execution state and its overview.
This avoids two consecutive execution events happening at the same time and messing up the state. Additionally we move the parsing cancel handle to the document where it belongs.
We will now put the proof view handling in the document manager. Since ther return type for the handle event function is becoming quite big, we turn it into a record.
Even in continuous mode, observe_id will now indicate where the user clicked.
…, etc..) back in documentManager
rtetley
force-pushed
the
cancel-event
branch
from
8c8249a to
cbb788d
Compare
rtetley
force-pushed
the
cancel-event
branch
from
3b4db9c to
c487d8b
Compare
rtetley
force-pushed
the
cancel-event
branch
from
c487d8b to
e13eadc
Compare
rtetley
force-pushed
the
cancel-event
branch
from
e13eadc to
0e8c72d
Compare
gares
reviewed
Nov 28, 2024
| (** [handle_event dpc ev] handles a parsing event for the document. One parsing event parses one line | ||
| and prepares the next parsing event. Finally once the full parsing is done, the final event returs | ||
| the id of the bottomost sentence of the prefix which has not changed since the previous validation | ||
| as well as the set of invalidated sentences. *) |
There was a problem hiding this comment.
I think you should build a record for the return type, so that we can name all these documents
gares
reviewed
Nov 28, 2024
| (** [init st opts uri text] initializes the document manager with initial vernac state | ||
| [st] on which command line opts will be set. *) | ||
| [st] on which command line opts will be set. [background] indicates if the document should | ||
| be executed in the background once it is parsed. *) |
gares
reviewed
Nov 28, 2024
| val clear_observe_id : state -> state | ||
| (** [clear_observe_id state] updates the state to make the observe_id None *) | ||
| id is updated. Finally if [background] is set to true, an execution is launched in | ||
| the background *) |
gares
reviewed
Nov 28, 2024
| (** resets Coq *) | ||
|
|
||
| val executed_ranges : state -> exec_overview | ||
| val executed_ranges : state -> Settings.Mode.t -> exec_overview |
There was a problem hiding this comment.
it is unclear what the mode is for here
rtetley
force-pushed
the
cancel-event
branch
from
e98c4aa to
7cfedb9
Compare
gares
reviewed
Dec 2, 2024
| (** [handle_event dpc ev] handles a parsing event for the document. One parsing event parses one line | ||
| and prepares the next parsing event. Finally once the full parsing is done, the final event returs | ||
| the id of the bottomost sentence of the prefix which has not changed since the previous validation | ||
| as well as the set of invalidated sentences. *) |
There was a problem hiding this comment.
When parsing ends, we still have two documents, hence two cancelation handles. This is a bit confusing: which document should the client keep?
There was a problem hiding this comment.
Not sure I catch your drift ? We have one "parsing" document which just became "parsed", and one "previous" document which is the version before all the new parsing events happened.
This makes the code way more readable
…k in continuous mode
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Trying another route from #937.
This time we use the SEL api to cancel events.
Currently does not seem to be working because of problem noted in gares/sel#10
Closes #682.
Closes #914.