[gnome-builder] prefs: add preferences to enable the Jedi plugin
- From: Christian Hergert <chergert src gnome org>
- To: commits-list gnome org
- Cc:
- Subject: [gnome-builder] prefs: add preferences to enable the Jedi plugin
- Date: Thu, 16 Jul 2015 21:10:38 +0000 (UTC)
commit 967d7314f7f7ba5f80e707d8665cd08c32e188b6
Author: Christian Hergert <christian hergert me>
Date: Wed Jul 15 21:56:22 2015 -0700
prefs: add preferences to enable the Jedi plugin
Simple preference to enable/disable the Jedi completion extension-type.
Since we aren't watching the signal type yet in IdeExtensionSetAdapter,
this requires a reload of the source view.
But at least its configurable now.
Also, long term, I want to see merge-able preference UI accessable from
plugins. We want to avoid the typical plugin-based configuration UI which
results in navigating features by their containing plugin (ugh).
data/ui/gb-preferences-page-insight.ui | 14 ++++++++++++++
1 files changed, 14 insertions(+), 0 deletions(-)
---
diff --git a/data/ui/gb-preferences-page-insight.ui b/data/ui/gb-preferences-page-insight.ui
index 1a62a59..128d83e 100644
--- a/data/ui/gb-preferences-page-insight.ui
+++ b/data/ui/gb-preferences-page-insight.ui
@@ -63,12 +63,26 @@
<property name="visible">true</property>
</object>
</child>
+ <child>
+ <object class="GbPreferencesSwitch" id="jedi_autocompletion">
+ <property name="settings">jedi_settings</property>
+ <property name="settings-schema-key">enabled</property>
+ <property name="title" translatable="yes">Suggest Completions using Jedi</property>
+ <property name="description" translatable="yes">Use Jedi for completions in the Python
language.</property>
+ <property name="size-group">control_group</property>
+ <property name="visible">true</property>
+ </object>
+ </child>
</object>
</child>
</template>
<object class="GSettings" id="insight_settings">
<property name="schema-id">org.gnome.builder.code-insight</property>
</object>
+ <object class="GSettings" id="jedi_settings">
+ <property name="path">/org/gnome/builder/extension-types/jedi_plugin/IdeCompletionProvider/</property>
+ <property name="schema-id">org.gnome.builder.extension-type</property>
+ </object>
<object class="GtkSizeGroup" id="control_group">
<property name="mode">horizontal</property>
</object>
[
Date Prev][
Date Next] [
Thread Prev][
Thread Next]
[
Thread Index]
[
Date Index]
[
Author Index]