max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/lean/elaborator): position on "unknown command" error

Browse source
This commit is contained in:
Sebastian Ullrich 2018-12-19 17:37:49 +01:00
parent 0911d16bc3
commit 0e5cfa5e8f
1 changed files with 5 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/init/lean/elaborator.lean
View file

@ -650,13 +650,11 @@ do
cmd ← current_command,
some n ← pure cmd.as_node |
error cmd $ "not a command: " ++ to_string cmd,
-- TODO(Sebastian): throw error on unknown command when we get serious
some elab ← pure $ elaborators.find n.kind.name |
-- TODO(Sebastian): reuse `log_message`
modify $ λ st, {st with messages := st.messages.add {filename := "foo", pos := ⟨1,0⟩, text := "unknown command: " ++ to_string n.kind.name}},
-- error cmd $ "unknown command: " ++ to_string n.kind.name,
catch elab $ λ e,
modify $ λ st, {st with messages := st.messages.add e})
catch
(do some elab ← pure $ elaborators.find n.kind.name |
error cmd $ "unknown command: " ++ to_string n.kind.name,
elab)
(λ e, modify $ λ st, {st with messages := st.messages.add e}))
elaborator.max_recursion,
match p with
| except.ok ((), st) := pure st.messages