# HG changeset patch
# User Goffi <goffi@goffi.org>
# Date 1521655626 -3600
# Node ID 1dfc5516dead13710a5daa461278e91f94d4145f
# Parent  0cb32e503aff14518d2d2b35670e64f87944ffb2
frontends (tools/misc): new FlagsHandler class, a simple class to help handling option flags

diff -r 0cb32e503aff -r 1dfc5516dead frontends/src/tools/misc.py
--- a/frontends/src/tools/misc.py	Wed Mar 21 19:07:00 2018 +0100
+++ b/frontends/src/tools/misc.py	Wed Mar 21 19:07:06 2018 +0100
@@ -60,3 +60,31 @@
             if callback is not None:
                 callback(self.input_history_tmp[index_tmp])
             self.input_history_index = index_tmp
+
+
+class FlagsHandler(object):
+    """Small class to handle easily option flags
+
+    the instance is initialized with an iterable
+    then attribute return True if flag is set, False else.
+    WARNING: If a flag is checked, it is removed (i.e. unset)
+        this is done to use bool(flags_handler) to check if all flags
+        have been used
+    """
+
+    def __init__(self, flags):
+        self.flags = set(flags or [])
+
+    def __getattr__(self, flag):
+        try:
+            self.flags.remove(flag)
+        except KeyError:
+            return False
+        else:
+            return True
+
+    def __len__(self):
+        return len(self.flags)
+
+    def __iter__(self):
+        return self.flags.__iter__()