semicolons between decls in namespaces

This commit is contained in:
rhiannon morris 2023-04-17 21:41:00 +02:00
parent 3fb8580f85
commit 6428d39ce1

View file

@ -326,6 +326,9 @@ defIntro : Grammar True Qty
defIntro = symbols [(Zero, "def0"), (Any, "defω")] defIntro = symbols [(Zero, "def0"), (Any, "defω")]
<|> resC "def" *> option Any (qty <* resC ".") <|> resC "def" *> option Any (qty <* resC ".")
skipSemis : Grammar False ()
skipSemis = ignore $ many $ resC ";"
export covering export covering
definition : Grammar True PDefinition definition : Grammar True PDefinition
definition = definition =
@ -339,7 +342,8 @@ mutual
export covering export covering
namespace_ : Grammar True PNamespace namespace_ : Grammar True PNamespace
namespace_ = namespace_ =
[|MkPNamespace (resC "namespace" *> mods) (braces $ many decl)|] [|MkPNamespace (resC "namespace" *> mods)
(braces $ many $ decl <* skipSemis)|]
export covering export covering
decl : Grammar True PDecl decl : Grammar True PDecl
@ -354,7 +358,6 @@ topLevel = [|PLoad load|]
export covering export covering
input : Grammar False (List PTopLevel) input : Grammar False (List PTopLevel)
input = skipSemis *> many (topLevel <* skipSemis) input = skipSemis *> many (topLevel <* skipSemis)
where skipSemis = ignore $ many $ resC ";"
public export public export