f3e3ebba81
This PR moves the validation of cross-package `import all` to Lake and the syntax validation of import keywords (`public`, `meta`, and `all`) to the two import parsers. It also fixes the error reporting of the fast import parser (`Lean.parseImports`) and adds positions to its errors.
3 lines
237 B
Text
3 lines
237 B
Text
moduleKeywords.lean:1:0-1:6: error: cannot use 'public import' without 'module'
|
|
moduleKeywords.lean:1:7-1:11: error: cannot use 'meta import' without 'module'
|
|
moduleKeywords.lean:2:7-2:10: error: cannot use 'import all' without 'module'
|