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

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

Browse source
This commit is contained in:
Sebastian Ullrich 2018-12-06 16:39:54 +01:00
parent e7a6746b6a
commit 599d5c6c76
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -497,9 +497,13 @@ do
(λ _, modify $ λ st, {st with messages := st.messages.add {filename := "foo", pos := ⟨1,0⟩, text := "elaborator.run: out of fuel"}})
(λ _, 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 n ← pure cmd.as_node | pure (),
some elab ← pure $ elaborators.find n.kind.name | pure (),
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})
elaborator.max_recursion,