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

feat(frontends/lean/server): use definitions_cache in the server object

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-10 20:02:50 -07:00
parent 34f0dedf46
commit 71583ba9c8
2 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/frontends/lean/server.cpp
View file

@ -79,6 +79,7 @@ void server::process_from(unsigned linenum) {
m_ios.set_options(s.m_options); m_ios.set_options(s.m_options);
parser p(s.m_env, m_ios, strm, m_fname.c_str(), false, 1, s.m_lds, s.m_eds, s.m_line, parser p(s.m_env, m_ios, strm, m_fname.c_str(), false, 1, s.m_lds, s.m_eds, s.m_line,
&m_snapshots, &m_info); &m_snapshots, &m_info);
p.set_cache(&m_cache);
p(); p();
} }

2
src/frontends/lean/server.h
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#pragma once #pragma once
#include <vector> #include <vector>
#include <string> #include <string>
#include "library/definitions_cache.h"
#include "frontends/lean/parser.h" #include "frontends/lean/parser.h"
#include "frontends/lean/info_manager.h" #include "frontends/lean/info_manager.h"
@ -26,6 +27,7 @@ class server {
snapshot m_empty_snapshot; snapshot m_empty_snapshot;
std::string m_fname; std::string m_fname;
unsigned m_from; unsigned m_from;
definitions_cache m_cache;
void read_file(std::string const & fname); void read_file(std::string const & fname);
void replace_line(unsigned linenum, std::string const & new_line); void replace_line(unsigned linenum, std::string const & new_line);