/usr/share/gps/library/closeold.py is in gnat-gps-common 6.1.2016-1ubuntu1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 | """
Automatically close old editors when a new one is opened.
This script can be used to keep only a limited number of editors
open at all times. It will automatically close the least recently
accessed editors when you open a new one.
"""
import GPS
from gps_utils import hook, interactive
maxeditors = GPS.Preference('Plugins/Close old editors/maxeditors')
maxeditors.create(
'Maximum number of editors',
'integer',
'Automatically close least recently accessed editors when more'
'than this number of editors are opened',
8)
def __close_editors_if_needed(keep=set()):
"""
If too many editors are opened, close one.
:param set keep: a set of files that should not be closed, even if
they are not pinned.
"""
opened = GPS.EditorBuffer.list()
toclose = len(opened) - maxeditors.get()
for ed in reversed(opened):
if toclose <= 0:
break
if (ed.file() not in keep
and not ed.is_modified()
and not getattr(ed, 'pinned', False)):
GPS.Console().write(
'Automatically closing %s\n' % ed.file().name())
ed.close(force=False)
toclose -= 1
@hook('file_edited')
def __on_file_edited(file):
"""
A new file has just been opened.
"""
__close_editors_if_needed(keep=set([file]))
@interactive(category='MDI', name='Pin Editor', filter='Source editor',
menu='/File/(Un)pin Editor', before='Close',
key='alt-p')
def __pin_file():
"""
Prevent a file from being closed automatically.
"""
ed = GPS.EditorBuffer.get(GPS.current_context().file(), open=False)
if ed:
ed.pinned = not getattr(ed, 'pinned', False)
for v in ed.views():
t = v.title().replace('^', '')
if ed.pinned:
GPS.MDI.get_by_child(v).rename('^%s' % t)
else:
GPS.MDI.get_by_child(v).rename(t)
|