From 599d5c6c76d4bf3c559563ca111dc2f4413582ca Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 6 Dec 2018 16:39:54 +0100 Subject: [PATCH] feat(library/init/lean/elaborator): log error on unknown command --- library/init/lean/elaborator.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index 5450de2adb..2177973547 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -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,