diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2025-12-16 17:10:31 +0100 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2025-12-16 17:10:31 +0100 |
| commit | ed546f3ce3d7c4e5840387beb2d89c8da05378ea (patch) | |
| tree | 8eab7129b4eea05159af7e820b4631897299bce5 /source/Syntax/Concrete.hs | |
| parent | 8e7d2c94d8449b8512fd6257534b4c593319b4ae (diff) | |
Add location info to implicit QED step
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 |