fix: expandMacroFns

We only keep trying other macros if the macro `m` produced
`unsupportedSyntax`. If the macro produced an error, we keep the
error.

@Kha This should fix the web demo.
This commit is contained in:
Leonardo de Moura 2020-06-15 14:39:36 -07:00
parent bc6dba89f3
commit 53dfd0d581

View file

@ -95,7 +95,13 @@ mkElabAttribute Macro `Lean.Elab.macroAttribute `builtinMacro `macro Name.anonym
private def expandMacroFns (stx : Syntax) : List Macro → MacroM Syntax
| [] => throw Macro.Exception.unsupportedSyntax
| m::ms => m stx <|> expandMacroFns ms
| m::ms =>
catch
(m stx)
(fun ex =>
match ex with
| Macro.Exception.unsupportedSyntax => expandMacroFns ms
| ex => throw ex)
def getMacros (env : Environment) : Macro :=
fun stx =>