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

Fix annoying problem when an integer occurs in the end of a command. Example 'Show 1.' was being parsed as 'Show 1.0'.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-21 11:57:22 -07:00
parent d750469667
commit 6534142fb9
2 changed files with 17 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/frontends/lean/lean_scanner.cpp
View file

@ -119,6 +119,14 @@ bool scanner::check_next(char c) {
return r;
}
bool scanner::check_next_is_digit() {
lean_assert(m_curr != EOF);
char c = m_stream.get();
bool r = '0' <= c && c <= '9';
m_stream.unget();
return r;
}
void scanner::read_comment() {
lean_assert(curr() == '*');
next();
@ -276,10 +284,15 @@ scanner::token scanner::read_number() {
q *= 10;
next();
} else if (c == '.') {
if (is_decimal)
// Num. is not a decimal. It should be at least Num.0
if (check_next_is_digit()) {
if (is_decimal)
break;
is_decimal = true;
next();
} else {
break;
is_decimal = true;
next();
}
} else {
break;
}

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

@ -40,6 +40,7 @@ protected:
void new_line() { m_line++; m_spos = 0; }
void next();
bool check_next(char c);
bool check_next_is_digit();
void read_comment();
name mk_name(name const & curr, std::string const & buf, bool only_digits);
token read_a_symbol();