Terry J. Reedy <[email protected]> added the comment:
All open files, up to the most recent 21 (and that could be increased) are in
the recent file list. Clicking on any name loads that file, unless it is
already loaded. The exception enforced in filelist.FileList.open, lines 29-32:
if key in self.dict:
edit = self.dict[key]
edit.top.wakeup()
return edit
I believe that we just need to ask, before the return, "Replace editor content
with file content?" and if yes, call edit.io.loadfile(filename).
----------
priority: low -> normal
_______________________________________
Python tracker <[email protected]>
<https://bugs.python.org/issue1721083>
_______________________________________
_______________________________________________
Python-bugs-list mailing list
Unsubscribe:
https://mail.python.org/mailman/options/python-bugs-list/archive%40mail-archive.com
