feat(frontends/lean): make set_option
affect fingerprints
This commit is contained in:
parent
498b2f681e
commit
e79c7d9852
3 changed files with 4 additions and 1 deletions
|
@ -277,7 +277,8 @@ environment set_option_cmd(parser & p) {
|
|||
throw parser_error("invalid option value, 'true', 'false', string, integer or decimal value expected", p.pos());
|
||||
}
|
||||
p.updt_options();
|
||||
return p.env();
|
||||
environment env = p.env();
|
||||
return update_fingerprint(env, p.get_options().hash());
|
||||
}
|
||||
|
||||
static name parse_class(parser & p) {
|
||||
|
|
|
@ -244,6 +244,7 @@ public:
|
|||
bool keep_new_thms() const { return m_keep_theorem_mode != keep_theorem_mode::DiscardAll; }
|
||||
|
||||
void updt_options();
|
||||
options get_options() const { return m_ios.get_options(); }
|
||||
template<typename T> void set_option(name const & n, T const & v) { m_ios.set_option(n, v); }
|
||||
|
||||
name mk_fresh_name() { return m_ngen.next(); }
|
||||
|
|
|
@ -33,6 +33,7 @@ public:
|
|||
unsigned size() const;
|
||||
bool contains(name const & n) const;
|
||||
bool contains(char const * n) const;
|
||||
unsigned hash() const { return m_value.hash(); }
|
||||
|
||||
bool get_bool(name const & n, bool default_value = false) const;
|
||||
int get_int(name const & n, int default_value = 0) const;
|
||||
|
|
Loading…
Reference in a new issue