File: prefs.py

package info (click to toggle)
gnat-gps 18-5
  • links: PTS, VCS
  • area: main
  • in suites: buster
  • size: 45,716 kB
  • sloc: ada: 362,679; python: 31,031; xml: 9,597; makefile: 1,030; ansic: 917; sh: 264; java: 17
file content (14 lines) | stat: -rw-r--r-- 427 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
 
# This is an example showing how to force setting of GPS preferences
# at start up.

from GPS import Preference, Hook


def on_gps_started(hook):
    # Set the preferences. You can adjust them at your convenience.
    Preference("Ada-Format-Operators").set(True)
    Preference("Ada-Ident-Casing").set("Smart_Mixed")
    Preference("Warnings-Src-Highlight-Color").set("#FFFF6D6D6D6D")


Hook("gps_started").add(on_gps_started)