agda2lagda 0.2023.6.9 → 0.2025.9.5
raw patch · 10 files changed
+43/−23 lines, 10 filesdep ~base
Dependency ranges changed: base
Files
- CHANGELOG.md +5/−0
- agda2lagda.cabal +9/−5
- src/LexicalStructure.hs +2/−0
- src/Markup.hs +12/−10
- src/Render.hs +5/−2
- src/Util.hs +6/−2
- test/golden/ClosingCommentInString.lagda.md +1/−1
- test/golden/ClosingCommentInString.lagda.tex +1/−1
- test/golden/Foo.lagda.md +1/−1
- test/golden/Foo.lagda.tex +1/−1
CHANGELOG.md view
@@ -1,5 +1,10 @@ # Revision history for agda2lagda +## 0.2025.9.5++* Fix `incomplete-patterns` warnings.+* Tested with GHC 8.0.2 - 9.14 alpha1.+ ## 0.2023.6.9 _West Pride revision._
agda2lagda.cabal view
@@ -1,7 +1,7 @@ cabal-version: 1.24 name: agda2lagda-version: 0.2023.6.9+version: 0.2025.9.5 synopsis: Translate .agda files into .lagda.tex files. description: Simple command line tool to convert plain Agda@@ -15,7 +15,7 @@ author: Andreas Abel maintainer: Andreas Abel <andreas.abel@cse.gu.se>-copyright: Andreas Abel, 2020-2023+copyright: Andreas Abel, 2020-2025 category: Dependent types, Development build-type: Simple@@ -32,8 +32,12 @@ test/golden/*.lagda.tex tested-with:- GHC == 9.6.2- GHC == 9.4.5+ GHC == 9.14.1+ GHC == 9.12.2+ GHC == 9.10.2+ GHC == 9.8.4+ GHC == 9.6.7+ GHC == 9.4.8 GHC == 9.2.8 GHC == 9.0.2 GHC == 8.10.7@@ -87,7 +91,7 @@ main-is: Tests.hs default-language: Haskell2010 ghc-options: -threaded- build-depends: base >= 4.11+ build-depends: base >= 4.11 && < 5 -- goldplate requires ghc >= 8.4 , process build-tool-depends: goldplate:goldplate
src/LexicalStructure.hs view
@@ -56,6 +56,8 @@ -- | Commented out code from block comments. pattern CommItem a = Item Comment a +{-# COMPLETE CodeItem, TextItem, CommItem #-}+ -- | Entry point for the parser of the lexical structure. parseItems
src/Markup.hs view
@@ -8,6 +8,8 @@ , gobbleTrailingBlockCommentClosers ) where +import qualified Data.List.NonEmpty as List1+ import Util import qualified LexicalStructure as L @@ -40,33 +42,33 @@ $ paragraphs s -- | A paragraph is a non-empty list of non-empty lines.-type Paragraph = [String]+type Paragraph = List1 String groupBullets :: [TextItem] -> [TextItem]-groupBullets = map joinItems . groupBy (\ a b -> all (isJust . isItemize) [a,b])+groupBullets = map joinItems . List1.groupBy (\ a b -> all (isJust . isItemize) [a,b]) where isItemize = \case Itemize ps -> Just ps _ -> Nothing- joinItems :: [TextItem] -> TextItem+ joinItems :: List1 TextItem -> TextItem joinItems is = -- In each group...- case mapMaybe isItemize is of+ case mapMaybe isItemize $ List1.toList is of -- ...either it is not Itemize- [] -> head is+ [] -> List1.head is -- or all are Itemize. pps -> Itemize $ concat pps -- | If the last line of a paragraph is just dashes or equal signs, we are a heading. detectMarkup :: Paragraph -> TextItem-detectMarkup ls@(l1:ls1)- | Just s <- bulleted l1 = Itemize [s:ls1]+detectMarkup ls@(l1 :| ls1)+ | Just s <- bulleted l1 = Itemize [s :| ls1] | all (== '=') l0 = Heading 1 $ unwords $ map trimLeft ls0 | all (== '-') l0 = Heading 2 $ unwords $ map trimLeft ls0 | otherwise = Paragraph ls where- (ls0, l) = initLast ls -- safe!+ (ls0, l) = initLast ls l0 = trimLeft l -- | If the line starts with @*@, return the rest.@@ -81,7 +83,7 @@ -- Preserves indentation. paragraphs :: String -> [Paragraph]-paragraphs = mapMaybe filterBlank . groupBy emptyOrNot . lines+paragraphs = mapMaybe filterBlank . List1.groupBy emptyOrNot . lines where emptyLine = null . trimLeft emptyOrNot = (==) `on` emptyLine@@ -92,7 +94,7 @@ -- | Text lines at the end of file consisting solely of words "-}" are -- discarded, to accommodate for a hack that makes it easy to comment -- out everything to the end of the file.--- https://github.com/agda/agda/issues/4953#issuecomment-702720296+-- <https://github.com/agda/agda/issues/4953#issuecomment-702720296> gobbleTrailingBlockCommentClosers :: [L.Item] -> [L.Item] gobbleTrailingBlockCommentClosers = updateLast $ \case
src/Render.hs view
@@ -8,6 +8,8 @@ , lagdaMd ) where +import qualified Data.List.NonEmpty as List1+ import qualified LexicalStructure as L import Options (Language, languageToHighlighter) import Markup@@ -35,12 +37,13 @@ renderTex :: TextItem -> String renderTex = \case- Paragraph p -> unlines p+ Paragraph p -> unlines $ List1.toList p Heading 1 s -> "\\heading{" ++ s ++ "}\n" Heading 2 s -> "\\subheading{" ++ s ++ "}\n"+ Heading _ _ -> error "Render.renderTex: headings are only supported of level 1 or 2" Itemize ps -> unlines $ concat $ [ [ "\\begin{itemize}\n" ]- , map (unlines . ("\\item" :)) ps+ , map (unlines . ("\\item" :) . List1.toList) ps , [ "\\end{itemize}" ] ]
src/Util.hs view
@@ -8,7 +8,11 @@ import Data.List as X (dropWhileEnd, groupBy) import Data.Maybe as X import Data.Semigroup as X+import Data.List.NonEmpty as X (pattern (:|))+import qualified Data.List.NonEmpty as List1 +type List1 = List1.NonEmpty+ (<&>) :: Functor f => f a -> (a -> b) -> f b (<&>) = flip (<$>) @@ -25,8 +29,8 @@ -- | Precondition: list non-empty. -initLast :: [a] -> ([a], a)-initLast as = (init as, last as)+initLast :: List1 a -> ([a], a)+initLast as = (List1.init as, List1.last as) -- * String manipulation
test/golden/ClosingCommentInString.lagda.md view
@@ -1,4 +1,4 @@-<!-- This file was automatically generated by agda2lagda 0.2023.6.9. -->+<!-- This file was automatically generated by agda2lagda 0.2025.9.5. --> This demonstrates a known issue: The parser is not aware of strings, thus,
test/golden/ClosingCommentInString.lagda.tex view
@@ -1,4 +1,4 @@-%% This file was automatically generated by agda2lagda 0.2023.6.9.+%% This file was automatically generated by agda2lagda 0.2025.9.5. This demonstrates a known issue: The parser is not aware of strings, thus,
test/golden/Foo.lagda.md view
@@ -1,4 +1,4 @@-<!-- This file was automatically generated by agda2lagda 0.2023.6.9. -->+<!-- This file was automatically generated by agda2lagda 0.2025.9.5. --> Sample non-literate Agda program ================================
test/golden/Foo.lagda.tex view
@@ -1,4 +1,4 @@-%% This file was automatically generated by agda2lagda 0.2023.6.9.+%% This file was automatically generated by agda2lagda 0.2025.9.5. \heading{Sample non-literate Agda program}