From 53dfd0d58198ecd82afd6bc9cad505c973852a28 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 15 Jun 2020 14:39:36 -0700
Subject: [PATCH] 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.
---
 src/Lean/Elab/Util.lean | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index aef6383b6a..a143a5a27d 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -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 =>