From 03ec9c2e1dc736d502d4bf07cc0523572e9fc1cf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 17 Dec 2021 15:59:33 +0100 Subject: [PATCH] chore: Cleanup the JSX parser a bit --- DocGen4/ToHtmlFormat.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean index 8afda02..4d6110b 100644 --- a/DocGen4/ToHtmlFormat.lean +++ b/DocGen4/ToHtmlFormat.lean @@ -52,7 +52,7 @@ open Parser PrettyPrinter declare_syntax_cat jsxElement declare_syntax_cat jsxChild -def jsxAttrVal : Parser := strLit <|> group ("{" >> termParser >> "}") <|> ("[" >> termParser >> "]") +def jsxAttrVal : Parser := strLit <|> group ("{" >> termParser >> "}") def jsxAttr : Parser := ident >> "=" >> jsxAttrVal -- JSXTextCharacter : SourceCharacter but not one of {, <, > or }