# HG changeset patch
# User Goffi <goffi@goffi.org>
# Date 1508481598 -7200
# Node ID a59f2abd970ea82256c4e49d27a834dae2038f91
# Parent  2e05921df16ab83c55ac91f822c0c738bb734f0d
frontends (xmlui): added ValueGetter.keys

diff -r 2e05921df16a -r a59f2abd970e frontends/src/tools/xmlui.py
--- a/frontends/src/tools/xmlui.py	Fri Oct 20 08:39:05 2017 +0200
+++ b/frontends/src/tools/xmlui.py	Fri Oct 20 08:39:58 2017 +0200
@@ -326,6 +326,9 @@
     def __getattr__(self, name):
         return self.__getitem__(name)
 
+    def keys(self):
+        return self.widgets.keys()
+
 
 class XMLUIPanel(XMLUIBase):
     """XMLUI Panel