JSON stream: support streaming a key-value pair to an object

Arrays already allow the equivalent operation, json_array_streamt::push_back(const jsont &)

Author: smowton

src/util/json_stream.h

@@ -169,6 +169,25 @@ class json_stream_objectt : public json_streamt
       return it->second;
   }
 
+  /// Push back a JSON element into the current object stream.
+  /// Note the pushed key won't be available via operator[], as it has been
+  /// output already.
+  /// Provided for compatibility with `jsont`.
+  /// \param key: new key to create in the streamed object
+  /// \param json: a non-streaming JSON element
+  void push_back(const std::string &key, const jsont &json)
+  {
+    PRECONDITION(open);
+    // Check the key is not already due to be output later:
+    PRECONDITION(!object.count(key));
+    // To ensure consistency of the output, we flush and
+    // close the current child stream before printing the given element.
+    output_child_stream();
+    output_delimiter();
+    jsont::output_key(out, key);
+    json.output_rec(out, indent + 1);
+  }
+
   json_stream_objectt &push_back_stream_object(const std::string &key);
   json_stream_arrayt &push_back_stream_array(const std::string &key);