hakyll-agda (empty) → 0.1
raw patch · 4 files changed
+258/−0 lines, 4 filesdep +Agdadep +basedep +containerssetup-changed
Dependencies added: Agda, base, containers, directory, filepath, hakyll, mtl, pandoc, transformers, xhtml
Files
- Hakyll/Web/Agda.hs +189/−0
- Setup.hs +2/−0
- css/agda.css +33/−0
- hakyll-agda.cabal +34/−0
+ Hakyll/Web/Agda.hs view
@@ -0,0 +1,189 @@+-- Parts of the code (specifically parts of `pairPositions' and `groupLiterate')+-- are taken from the Agda.Interaction.Highlighting.HTML module of Agda, see+-- <http://code.haskell.org/Agda/LICENSE> for the license and the copyright+-- information for that code.+module Hakyll.Web.Agda+ ( markdownAgda+ , pandocAgdaCompilerWith+ , pandocAgdaCompiler+ ) where++import Control.Applicative+import Data.Char+import Data.Function+import Data.List+import Data.Maybe+import Data.Monoid++import Control.Monad.Error (catchError, throwError)+import Control.Monad.IO.Class (liftIO)+import Control.Monad.State (get)+import qualified Data.Map as Map+import System.Directory+import System.Exit (exitFailure)+import System.FilePath+import Text.XHtml.Strict++import Agda.Interaction.Highlighting.Precise+import qualified Agda.Interaction.Imports as Imp+import Agda.Interaction.Options+import Agda.Syntax.Abstract.Name (toTopLevelModuleName)+import Agda.Syntax.Common+import Agda.Syntax.Concrete.Name (TopLevelModuleName)+import Agda.TypeChecking.Errors+import Agda.TypeChecking.Monad (TCM)+import qualified Agda.TypeChecking.Monad as TCM+import Agda.Utils.FileName+import qualified Agda.Utils.IO.UTF8 as UTF8+import Hakyll.Core.Compiler+import Hakyll.Core.Identifier+import Hakyll.Core.Item+import Hakyll.Web.Pandoc+import Text.Pandoc++checkFile :: AbsolutePath -> TCM TopLevelModuleName+checkFile file =+ do TCM.resetState+ toTopLevelModuleName . TCM.iModuleName . fst <$> Imp.typeCheck file++getModule :: TopLevelModuleName -> TCM (HighlightingInfo, String)+getModule m =+ do Just mi <- TCM.getVisitedModule m+ Just f <- Map.lookup m . TCM.stModuleToSource <$> get+ s <- liftIO . UTF8.readTextFile . filePath $ f+ return (TCM.iHighlighting (TCM.miInterface mi), s)++pairPositions :: HighlightingInfo -> String -> [(Integer, String, MetaInfo)]+pairPositions info contents =+ map (\cs@((mi, (pos, _)) : _) -> (pos, map (snd . snd) cs, maybe mempty id mi)) .+ groupBy ((==) `on` fst) .+ map (\(pos, c) -> (Map.lookup pos infoMap, (pos, c))) .+ zip [1..] $+ contents+ where+ infoMap = toMap (decompress info)++-- TODO make these more accurate+beginCode :: String -> MetaInfo -> Bool+beginCode s _ = isInfixOf "\\begin{code}" s++endCode :: String -> MetaInfo -> Bool+endCode s _ = isInfixOf "\\end{code}" s++groupLiterate :: [(Integer, String, MetaInfo)]+ -> [Either String [(Integer, String, MetaInfo)]]+groupLiterate = begin+ where+ -- TODO Make the spacing cleaner+ begin contents =+ let (com, rest) = span (notCode beginCode) contents+ in Left ("\n\n" ++ concat [s | (_, s, _) <- com] ++ "\n\n") :+ trimTop (end rest)++ end [] = []+ end mis =+ case span (notCode endCode) mis of+ (a, e : b) -> Right (a ++ [trimEnd e]) : begin b+ _ -> error "malformed file"++ notCode :: (String -> MetaInfo -> Bool) -> (Integer, String, MetaInfo) -> Bool+ notCode f (_, s, mi) = not (f s mi)++ trimTop (Right ((pos, s, mi) : rs) : rest) =+ Right ((pos, dropWhile isSpace s, mi) : rs) : rest+ trimTop x = x++ trimEnd (pos, s, mi) = (pos, reverse (dropWhile isSpace (reverse s)), mi)++annotate :: TopLevelModuleName -> Integer -> MetaInfo -> Html -> Html+annotate m pos mi = anchor ! attributes+ where+ attributes = [name (show pos)] +++ fromMaybe [] (definitionSite mi >>= link) +++ (case classes of [] -> []; cs -> [theclass (unwords cs)])++ classes = maybe [] noteClasses (note mi) +++ otherAspectClasses (otherAspects mi) +++ maybe [] aspectClasses (aspect mi)++ aspectClasses (Name mKind op) =+ let kindClass = maybe [] ((: []) . showKind) mKind++ showKind (Constructor Inductive) = "InductiveConstructor"+ showKind (Constructor CoInductive) = "CoinductiveConstructor"+ showKind k = show k++ opClass = if op then ["Operator"] else []+ in kindClass ++ opClass+ aspectClasses a = [show a]++ otherAspectClasses = map show++ -- Notes are not included.+ noteClasses _ = []++ link (m', pos') = if m == m'+ then Just [href ("#" ++ show pos')]+ else Nothing++toMarkdown :: String+ -> TopLevelModuleName -> [Either String [(Integer, String, MetaInfo)]]+ -> String+toMarkdown classpr m contents =+ concat [ case c of+ Left s -> s+ Right cs ->+ let h = pre . mconcat $ [ (annotate m pos mi (stringToHtml s))+ | (pos, s, mi) <- cs ]+ in renderHtmlFragment (h ! [theclass classpr])+ | c <- contents ]++convert :: String -> TopLevelModuleName -> TCM String+convert classpr m =+ do (info, contents) <- getModule m+ return . toMarkdown classpr m . groupLiterate . pairPositions info $ contents++markdownAgda :: CommandLineOptions -> String -> FilePath -> IO String+markdownAgda opts classpr fp =+ do r <- TCM.runTCM $ catchError (TCM.setCommandLineOptions opts >>+ checkFile (mkAbsolute fp) >>= convert classpr)+ $ \err -> do s <- prettyError err+ liftIO (putStrLn s)+ throwError err+ case r of+ Right s -> return (dropWhile isSpace s)+ Left _ -> exitFailure++isAgda :: Item a -> Bool+isAgda i = ex == ".lagda"+ where ex = snd . splitExtension . toFilePath . itemIdentifier $ i++saveDir :: IO a -> IO a+saveDir m = do origDir <- getCurrentDirectory; m <* setCurrentDirectory origDir++pandocAgdaCompilerWith :: ReaderOptions -> WriterOptions -> CommandLineOptions+ -> Compiler (Item String)+pandocAgdaCompilerWith ropt wopt aopt =+ do i <- getResourceBody+ if isAgda i+ then cached cacheName $+ do fp <- getResourceFilePath+ -- TODO get rid of the unsafePerformIO, and have a more solid+ -- way of getting the absolute path+ unsafeCompiler . saveDir $+ do -- We set to the directory of the file, we assume that+ -- the agda files are in one flat directory which might+ -- not be not the one where Hakyll is ran in.+ abfp <- canonicalizePath fp+ setCurrentDirectory (dropFileName abfp)+ s <- markdownAgda aopt "Agda" abfp+ let i' = i {itemBody = s}+ return (writePandocWith wopt (readMarkdown ropt <$> i'))+ else pandocCompilerWith ropt wopt+ where+ cacheName = "LiterateAgda.pandocAgdaCompilerWith"++pandocAgdaCompiler :: Compiler (Item String)+pandocAgdaCompiler =+ pandocAgdaCompilerWith defaultHakyllReaderOptions defaultHakyllWriterOptions+ defaultOptions
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ css/agda.css view
@@ -0,0 +1,33 @@+/* Aspects. */+pre.Agda a.Comment { color: #B22222 }+pre.Agda a.Keyword { color: #CD6600 }+pre.Agda a.String { color: #B22222 }+pre.Agda a.Number { color: #A020F0 }+pre.Agda a.Symbol { color: #404040 }+pre.Agda a.PrimitiveType { color: #0000CD }+pre.Agda a.Operator {}++/* NameKinds. */+pre.Agda a.Bound { color: black }+pre.Agda a.InductiveConstructor { color: #008B00 }+pre.Agda a.CoinductiveConstructor { color: #8B7500 }+pre.Agda a.Datatype { color: #0000CD }+pre.Agda a.Field { color: #EE1289 }+pre.Agda a.Function { color: #0000CD }+pre.Agda a.Module { color: #A020F0 }+pre.Agda a.Postulate { color: #0000CD }+pre.Agda a.Primitive { color: #0000CD }+pre.Agda a.Record { color: #0000CD }++/* OtherAspects. */+pre.Agda a.DottedPattern {}+pre.Agda a.UnsolvedMeta { color: black; background: yellow }+pre.Agda a.UnsolvedConstraint { color: black; background: yellow }+pre.Agda a.TerminationProblem { color: black; background: #FFA07A }+pre.Agda a.IncompletePattern { color: black; background: #F5DEB3 }+pre.Agda a.Error { color: red; text-decoration: underline }+pre.Agda a.TypeChecks { color: black; background: #ADD8E6 }++/* Standard attributes. */+pre.Agda a { text-decoration: none }+pre.Agda a[href]:hover { background-color: #B4EEB4 }
+ hakyll-agda.cabal view
@@ -0,0 +1,34 @@+Cabal-version: >= 1.6+Name: hakyll-agda+Version: 0.1+Author: Francesco Mazzoli (f@mazzo.li)+Maintainer: Francesco Mazzoli (f@mazzo.li)+Build-Type: Simple+License: BSD3+Build-Type: Simple+Category: Web+Synopsis: Wrapper to integrate literate Agda files with Hakyll+Tested-With: GHC==7.4.1+Homepage: https://github.com/bitonic/website+Bug-Reports: https://github.com/bitonic/website/issues+Description:+ Simple module useful to generate blog posts from literate Agda files.+Data-Files: css/agda.css++source-repository head+ type: git+ location: git://github.com/bitonic/website.git++Library+ Build-Depends: base >= 3 && < 5,+ hakyll >= 4.2 && < 5,+ Agda >= 2.3 && < 3,+ pandoc >= 1.10 && < 2,+ xhtml >= 3000.2 && < 3000.3,+ filepath >= 1.3 && < 2,+ directory >= 1.1 && < 2,+ containers >= 0.4.2 && < 0.5,+ mtl >= 2.1 && < 3,+ transformers >= 0.3 && < 0.4+ GHC-Options: -Wall+ Exposed-Modules: Hakyll.Web.Agda