From 57ed29e814d2d9f8eb93374cf13138befde2e144 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 19 Aug 2020 09:57:58 -0700 Subject: [PATCH] revert: `panic!` changes @Kha I am reverting this change for now. I understand that the "default-value" approach is bad for debugging, and it does not produce good error messages, but at least the frontend will not "panic" when users add a bad macro. After we switch to the new frontend, we can have a monadic `getArg` and `getArgs` in the Elab and Macro monads which produces an "unexpected syntax" error message. I say we wait for the new frontend because we will be able to write `(<- s.getArg)` inside of expressions. --- src/Init/LeanInit.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean index c76f92ad11..98fd2bd62a 100644 --- a/src/Init/LeanInit.lean +++ b/src/Init/LeanInit.lean @@ -223,12 +223,12 @@ def isOfKind : Syntax → SyntaxNodeKind → Bool def getArg (stx : Syntax) (i : Nat) : Syntax := match stx with | Syntax.node _ args => args.get! i -| _ => panic! "Syntax.getArg: not a node" +| _ => Syntax.missing -- panic! "Syntax.getArg: not a node" def getArgs (stx : Syntax) : Array Syntax := match stx with | Syntax.node _ args => args -| _ => panic! "Syntax.getArgs: not a node" +| _ => #[] -- panic! "Syntax.getArgs: not a node" /-- Retrieve the left-most leaf's info in the Syntax tree. -/ partial def getHeadInfo : Syntax → Option SourceInfo