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 this._editor_font_size = (int) value;
28 if (this.css != null) {
29 this.css.load_from_string(
30 ".code-editor { font: %dpx monospace; }".printf((int) value)
35 this.editor_font_size_updated();
39 public bool editor_font_size_inchange = false;
40 public signal void editor_font_size_updated();
43 // things we look after..
44 Gtk.CssProvider? css = null;
51 this.css = new Gtk.CssProvider();
52 this.editor_font_size = 10;
53 Gtk.StyleContext.add_provider_for_display(
54 Gdk.Display.get_default(),
56 Gtk.STYLE_PROVIDER_PRIORITY_APPLICATION
79 public void loadOld() {