michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/parser): save snapshots

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-06 18:31:53 -07:00
parent 9b765a2a06
commit 1ba9a92df2
2 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/frontends/lean/parser.cpp
View file

@ -1136,6 +1136,7 @@ bool parser::parse_commands() {
switch (curr()) {
case scanner::token_kind::CommandKeyword:
parse_command();
save_snapshot();
break;
case scanner::token_kind::ScriptBlock:
parse_script();
@ -1165,6 +1166,13 @@ void parser::add_delayed_theorem(environment const & env, name const & n, level_
m_theorem_queue.add(env, n, ls, get_local_level_decls(), t, v);
}
void parser::save_snapshot() {
if (!m_snapshot_vector)
return;
if (m_snapshot_vector->empty() || static_cast<int>(m_snapshot_vector->back().m_line) != m_scanner.get_line())
m_snapshot_vector->push_back(snapshot(m_env, m_local_level_decls, m_local_decls, m_ios.get_options(), m_scanner.get_line()));
}
bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions,
unsigned num_threads) {
parser p(env, ios, in, strm_name, use_exceptions, num_threads);

1
src/frontends/lean/parser.h
View file

@ -151,6 +151,7 @@ class parser {
void push_local_scope();
void pop_local_scope();
void save_snapshot();
public:
parser(environment const & env, io_state const & ios,