# HG changeset patch
# User Goffi <goffi@goffi.org>
# Date 1489443306 -3600
# Node ID 322948499db08f27130ccf12946641a989ce9878
# Parent  33b82250eaddffda8f86a308a47a9b20490da5f7
jp (output dict): added color and no-header option

diff -r 33b82250eadd -r 322948499db0 frontends/src/jp/output_std.py
--- a/frontends/src/jp/output_std.py	Mon Mar 13 23:14:00 2017 +0100
+++ b/frontends/src/jp/output_std.py	Mon Mar 13 23:15:06 2017 +0100
@@ -20,6 +20,7 @@
 
 
 from sat_frontends.jp.constants import Const as C
+from sat.tools.common.ansi import ANSI as A
 import json
 
 __outputs__ = ["Simple", "Json"]
@@ -45,8 +46,16 @@
         self.host.disp(u'\n'.join(data))
 
     def dict(self, data):
-        for k, v in data:
-            self.host.disp((u'{key}: {value}'.format(key=k, value=v)))
+        options = self.host.parse_output_options()
+        self.host.check_output_options({u'no-header'}, options)
+        show_header = not u'no-header' in options
+        for k, v in data.iteritems():
+            if show_header:
+                header = A.color(A.BOLD, A.FG_YELLOW, k) + u': '
+            else:
+                header = u''
+
+            self.host.disp((u'{header}{value}'.format(header=header, value=v)))
 
 
 class Json(object):