From 0e5cfa5e8ff74ee2913ff1e48cb0df44cf1b5ef7 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 19 Dec 2018 17:37:49 +0100
Subject: [PATCH] feat(library/init/lean/elaborator): position on "unknown
 command" error

---
 library/init/lean/elaborator.lean | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean
index f90b548d0b..12dda551a8 100644
--- a/library/init/lean/elaborator.lean
+++ b/library/init/lean/elaborator.lean
@@ -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