docstring const & prettyCounter() const { return pretty_counter_; }
/// Updates only the label string, doesn't handle undo nor references.
void updateLabel(docstring const & new_label);
docstring const & prettyCounter() const { return pretty_counter_; }
/// Updates only the label string, doesn't handle undo nor references.
void updateLabel(docstring const & new_label);