/usr/share/gps/plug-ins/zoom.py is in gnat-gps-common 6.1.1-1.
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 | """This scripts adds a menu for quickly changing font sizes
When this plug-in is loaded, it adds a new menu /Edit/Text Size which
provides a fast access to the preferences related to font sizes. This
can be used to quickly zoom on the text.
The modification is permanent, since it modifies the actual preferences,
and the new text size will be active when GPS is relaunched later on.
"""
#############################################################################
# No user customization below this line
#############################################################################
from GPS import *
import gi
gi.require_version('Gtk', '3.0')
from gi.repository import Pango
import gps_utils
def zoom_pref(pref, factor, save=True):
p = Preference(pref)
(font, fg, bg) = p.get().split("@")
descr = Pango.FontDescription(font)
descr.set_size(int(descr.get_size() * factor))
p.set(descr.to_string() + "@" + fg + "@" + bg, save)
def zoom(factor):
zoom_pref("Src-Editor-Reference-Style", factor, True)
@gps_utils.interactive(name="increase text size", category="Editor")
def zoom_in():
"""Increase the size of fonts in the source editors.
This impacts the corresponding preferences."""
zoom(1.2)
@gps_utils.interactive(name="decrease text size", category="Editor")
def zoom_out():
"""Decrease the size of fonts in the source editors.
This impacts the corresponding preferences."""
zoom(1 / 1.2)
|