-
-
Notifications
You must be signed in to change notification settings - Fork 2.6k
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.
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
Detect and warn when document is modified externally (#1125) #12504
base: master
Are you sure you want to change the base?
Conversation
Add a new CheckModificationHandler that reacts to document changes. Trigger an asynchronous poll of the file metadata, which will eventually update a new `externally_modified` field in Document. Also exposes the last_saved_time in Document to the helix-view crate, so that the logic for comparing it to the file mtime can take place in Editor (i.e. without borrowing Document). This commit doesn't actually make the externally_modified field user-visible in any way, it just populates it in the background.
Use "+", "-" or "!" respectively to indicate whether there is an internal modification, external modification, or both.
This means the status line will update as soon as the file change is detected, rather than waiting for some subsequent editor event.
A lot can happen in 2s. This feels more snappy.
Sets the editor status to instruct the user to resolve the external modification conflict with `:write!` or `:reload`. This triggers after every document change (modulo debounce), so it flashes quite a lot, but that's more desirable than wasting edits.
let title = match (is_modified, externally_modified) { | ||
(true, true) => "[!]", | ||
(true, false) => "[+]", | ||
(false, true) => "[-]", |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
(false, true) => "[-]", | |
(false, true) => "[~]", |
-
does not have connotations of "this file has been externally modified". ~
may be a better suited symbol for this (for example, often used in diffs to indicate changed lines. -
usually means something was removed)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not particularly opinionated about the symbol here, but let me explain the reasoning for -
and see what you think:
-
is the logical opposite of +
. +
is already used to indicate that the current state is ahead of the base file. -
makes sense for the opposite, i.e. the editor state is behind the base file. Of course this is only in terms of timestamps, none of these actually concern the content (i.e. the existing +
is already used in the case where, say, you remove some lines and haven't saved yet).
Still prefer ~
?
A pragmatic solution to #1125.
Whenever a document is changed within helix, check the mtime from the file system to see if it is different than the last-known save time. If it is:
+
,-
or!
respectively to indicate whether there is an internal modification, external modification, or both (a conflict).Reloading is not forced on the user; just encouraged.
This PR does not do any fancy registration for push notifications ala inotify/fsevent, nor is it suitable for keeping LSPs in sync. But it does solve the problem of warning users before they invest time into making edits that will either clobber or need to be manually merged with other changes later.
The heuristic it uses (using the file system mtime) isn't perfect, but it matches the existing logic that
:write
applies today to detect conflicts.