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

Refactor observe id #693

Merged
merged 4 commits into from
Nov 30, 2023
Merged

Refactor observe id #693

merged 4 commits into from
Nov 30, 2023

Conversation

rtetley
Copy link
Collaborator

@rtetley rtetley commented Nov 23, 2023

This pull request adresses some inconsistencies with the observe id.
By default now the observe id is None in continuous mode and Top (for top of the document) or (Id id) when on a specific sentence.

@rtetley
Copy link
Collaborator Author

rtetley commented Nov 23, 2023

A problem is now changing the settings...
If we change from Manual to Continuous, it's easy, we just pot observe_id = None
If we change form Continuous to Manual it is tricky, how to we assign observe_id ? Some ideas: we just assign it to top, or we look for the last sentence id which was executed and we assign it to that.

@gares
Copy link
Member

gares commented Nov 24, 2023

I would do the former, since computations are cached, we lose nothing: advancing forward will be instantaneous up to the point you would use in the latter option

@rtetley
Copy link
Collaborator Author

rtetley commented Nov 24, 2023

Definitely simpler, however since decorations in manual mode depend upon the observe_id, the user will be under the impression that the execution state has been reset. Not great UX I guess.

@rtetley rtetley requested a review from maximedenes November 24, 2023 14:22
@gares
Copy link
Member

gares commented Nov 24, 2023

If you are in continuons mode you should not see any green area, and hence going to manual is the same (there is no green disappearing).

Or you refer to other decorations?

@rtetley rtetley force-pushed the refactor_observe_id branch from bb9022d to e73076b Compare November 27, 2023 09:13
@rtetley rtetley changed the title Refactor observen id Refactor observe id Nov 27, 2023
@rtetley rtetley marked this pull request as ready for review November 27, 2023 09:13
@rtetley
Copy link
Collaborator Author

rtetley commented Nov 27, 2023

You're right. I've changed the code so to reset the decorations when we move from manual to continuous mode as well !

@rtetley rtetley requested a review from gares November 27, 2023 12:56
@rtetley
Refactor observe_id.
8e967dd 
observe_id is only used in manual mode. In continuous mode it is now null.
In manual mode we now introduce the Top type to indicate that observe id is currently at
the top of the document.
@rtetley
Correct unit tests.
7a06d45
@rtetley
Reset view when switching from continuous to manual.
22784f6
@rtetley
Fix Hashtbl.find_opt regression.
d17a89c
@rtetley rtetley force-pushed the refactor_observe_id branch from af0ada3 to d17a89c Compare November 30, 2023 14:04
@rtetley rtetley merged commit e0a34f9 into main Nov 30, 2023
9 checks passed
@rtetley rtetley deleted the refactor_observe_id branch February 7, 2024 11:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@maximedenes maximedenes Awaiting requested review from maximedenes

@gares gares Awaiting requested review from gares

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@rtetley @gares