3 File to handle global settings
4 In theory this should be stored in GLib.Settings - but since that requires a load of infrastructure to create
5 we will stick to "~/.config/roobuilder.json" for now
8 we used to store it in '.Builder/Project.list' .. but that's going to change..
11 // this should be available via BuilderApplicaiton.settings
16 public class Settings : Object {
18 // things that can be set..
20 private int _editor_font_size = 10;
21 public double editor_font_size {
23 return (double) this._editor_font_size;
26 GLib.debug("updated to %d", (int) value );
27 if (value < 6 || value > 50) {
30 this._editor_font_size = (int) value;
31 if (this.css != null) {
32 this.css.load_from_string(
33 ".code-editor { font: %dpx monospace; }".printf((int) value)
38 this.editor_font_size_updated();
42 public bool editor_font_size_inchange = false;
43 public signal void editor_font_size_updated();
46 // things we look after..
47 Gtk.CssProvider? css = null;
54 this.css = new Gtk.CssProvider();
55 this.editor_font_size = 10;
56 Gtk.StyleContext.add_provider_for_display(
57 Gdk.Display.get_default(),
59 Gtk.STYLE_PROVIDER_PRIORITY_APPLICATION
82 public void loadOld() {