diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index d7424d59cf..556e1def95 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -353,9 +353,9 @@ scanner::token scanner::read_script_block() { next(); if (c1 == '*') { char c2 = curr(); - next(); if (c2 == EOF) throw_exception("unexpected end of script"); + next(); if (c2 == ')') { return token::ScriptBlock; } else { diff --git a/tests/lean/scan_error1.lean b/tests/lean/scan_error1.lean new file mode 100644 index 0000000000..ab902fc293 --- /dev/null +++ b/tests/lean/scan_error1.lean @@ -0,0 +1,4 @@ +.. +print "begin" +.. +print "done" \ No newline at end of file diff --git a/tests/lean/scan_error1.lean.expected.out b/tests/lean/scan_error1.lean.expected.out new file mode 100644 index 0000000000..2b1577cee5 --- /dev/null +++ b/tests/lean/scan_error1.lean.expected.out @@ -0,0 +1,3 @@ + Set: pp::colors + Set: pp::unicode +Error (line: 1, pos: 3) invalid character sequence, '...' ellipsis expected diff --git a/tests/lean/scan_error2.lean b/tests/lean/scan_error2.lean new file mode 100644 index 0000000000..64b76bed64 --- /dev/null +++ b/tests/lean/scan_error2.lean @@ -0,0 +1 @@ +(* print("from lua") \ No newline at end of file diff --git a/tests/lean/scan_error2.lean.expected.out b/tests/lean/scan_error2.lean.expected.out new file mode 100644 index 0000000000..c4b6a53015 --- /dev/null +++ b/tests/lean/scan_error2.lean.expected.out @@ -0,0 +1,3 @@ + Set: pp::colors + Set: pp::unicode +Error (line: 1, pos: 21) unexpected end of script diff --git a/tests/lean/scan_error3.lean b/tests/lean/scan_error3.lean new file mode 100644 index 0000000000..a45f48fe58 --- /dev/null +++ b/tests/lean/scan_error3.lean @@ -0,0 +1 @@ +(* print("from lua") * \ No newline at end of file diff --git a/tests/lean/scan_error3.lean.expected.out b/tests/lean/scan_error3.lean.expected.out new file mode 100644 index 0000000000..3adacfe196 --- /dev/null +++ b/tests/lean/scan_error3.lean.expected.out @@ -0,0 +1,3 @@ + Set: pp::colors + Set: pp::unicode +Error (line: 1, pos: 23) unexpected end of script diff --git a/tests/lean/scan_test1.lean b/tests/lean/scan_test1.lean new file mode 100644 index 0000000000..360dca6d53 --- /dev/null +++ b/tests/lean/scan_test1.lean @@ -0,0 +1 @@ +print 10.0. \ No newline at end of file diff --git a/tests/lean/scan_test1.lean.expected.out b/tests/lean/scan_test1.lean.expected.out new file mode 100644 index 0000000000..4c6d370253 --- /dev/null +++ b/tests/lean/scan_test1.lean.expected.out @@ -0,0 +1,3 @@ + Set: pp::colors + Set: pp::unicode +10 diff --git a/tests/lean/scan_test2.lean b/tests/lean/scan_test2.lean new file mode 100644 index 0000000000..ecbb75f5b0 --- /dev/null +++ b/tests/lean/scan_test2.lean @@ -0,0 +1,7 @@ +(* + a = 1 * +2 + print("a") +*) + +prnt "fail" \ No newline at end of file diff --git a/tests/lean/scan_test2.lean.expected.out b/tests/lean/scan_test2.lean.expected.out new file mode 100644 index 0000000000..70a136889d --- /dev/null +++ b/tests/lean/scan_test2.lean.expected.out @@ -0,0 +1,4 @@ + Set: pp::colors + Set: pp::unicode +a +Error (line: 7, pos: 0) Command expected