mirror of
https://github.com/python/cpython.git
synced 2026-04-20 10:51:00 +00:00
gh-94523: IDLE: Detect file if modified and prompt the user to refresh (GH-145625)
This commit is contained in:
parent
f445d2e866
commit
6e2272d0b1
2 changed files with 22 additions and 0 deletions
|
|
@ -312,6 +312,9 @@ def __init__(self, flist=None, filename=None, key=None, root=None):
|
|||
else:
|
||||
self.update_menu_state('options', '*ine*umbers', 'disabled')
|
||||
|
||||
self.mtime = self.last_mtime()
|
||||
text_frame.bind('<FocusIn>', self.focus_in_event)
|
||||
|
||||
def handle_winconfig(self, event=None):
|
||||
self.set_width()
|
||||
|
||||
|
|
@ -1027,6 +1030,8 @@ def get_saved(self):
|
|||
|
||||
def set_saved(self, flag):
|
||||
self.undo.set_saved(flag)
|
||||
if flag:
|
||||
self.mtime = self.last_mtime()
|
||||
|
||||
def reset_undo(self):
|
||||
self.undo.reset_undo()
|
||||
|
|
@ -1112,6 +1117,21 @@ def _close(self):
|
|||
# unless override: unregister from flist, terminate if last window
|
||||
self.close_hook()
|
||||
|
||||
def last_mtime(self):
|
||||
file = self.io.filename
|
||||
return os.path.getmtime(file) if file else 0
|
||||
|
||||
def focus_in_event(self, event):
|
||||
mtime = self.last_mtime()
|
||||
if self.mtime != mtime:
|
||||
self.mtime = mtime
|
||||
if self. askyesno(
|
||||
'Reload', '"%s"\n\nThis script has been modified by another program.'
|
||||
'\nDo you want to reload it?' % self.io.filename, parent=self.text):
|
||||
self.io.loadfile(self.io.filename)
|
||||
else:
|
||||
self.set_saved(False)
|
||||
|
||||
def load_extensions(self):
|
||||
self.extensions = {}
|
||||
self.load_standard_extensions()
|
||||
|
|
|
|||
|
|
@ -0,0 +1,2 @@
|
|||
Detect file if modified at local disk and prompt to ask refresh. Patch by
|
||||
Shixian Li.
|
||||
Loading…
Add table
Add a link
Reference in a new issue