diff options
Diffstat (limited to 'source/Syntax/Concrete.hs')
| -rw-r--r-- | source/Syntax/Concrete.hs | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index 4c34b57..30e57ea 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -416,7 +416,7 @@ grammar lexicon@Lexicon{..} = mdo blockAxiom <- rule $ uncurry3 BlockAxiom <$> envPos "axiom" axiom blockLemma <- rule $ uncurry3 BlockLemma <$> lemmaEnv lemma - blockProof <- rule $ uncurry BlockProof <$> envPos_ "proof" proof + blockProof <- rule $ uncurry3 BlockProof <$> envStartEndLocation "proof" proof blockDefn <- rule $ uncurry3 BlockDefn <$> envPos "definition" defn blockAbbr <- rule $ uncurry3 BlockAbbr <$> envPos "abbreviation" abbreviation blockData <- rule $ uncurry BlockData <$> envPos_ "datatype" datatype @@ -647,6 +647,9 @@ envPos kind body = do envPos_ :: Text -> Prod r Text (Located Token) a -> Prod r Text (Located Token) (Location, a) envPos_ kind body = (,) <$> begin kind <*> (optional label *> body) <* end kind +envStartEndLocation :: Text -> Prod r Text (Located Token) a -> Prod r Text (Located Token) (Location, a, Location) +envStartEndLocation kind body = (,,) <$> begin kind <*> (optional label *> body) <*> end kind + env_ :: Text -> Prod r Text (Located Token) a -> Prod r Text (Located Token) a env_ kind body = begin kind *> optional label *> body <* end kind |