agda-snippets-hakyll (empty) → 0.1
raw patch · 4 files changed
+187/−0 lines, 4 filesdep +agda-snippetsdep +basedep +directorysetup-changed
Dependencies added: agda-snippets, base, directory, filepath, hakyll, network-uri, pandoc, pandoc-types
Files
- LICENSE +30/−0
- Setup.hs +2/−0
- agda-snippets-hakyll.cabal +33/−0
- src/Hakyll/Contrib/Agda.hs +122/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2015, Liam O'Connor++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Liam O'Connor nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ agda-snippets-hakyll.cabal view
@@ -0,0 +1,33 @@+name: agda-snippets-hakyll+version: 0.1+synopsis: Literate Agda support using agda-snippets, for Hakyll pages.+description: This library provides basic functions to use in Hakyll web-pages to generate+ colourised and hyperlinked Agda source code snippets for literate Agda documents.+ .+ It makes use of the @agda-snippets@ library and will (hopefully) be kept up to + date with the latest Agda versions.+homepage: https://github.com/liamoc/agda-snippets#readme+license: BSD3+license-file: LICENSE+author: Liam O'Connor+maintainer: liamoc@cse.unsw.edu.au+copyright: Liam O'Connor, 2015+category: Dependent Types+build-type: Simple+cabal-version: >=1.10++library+ build-depends: base >=4.7 && <4.9, agda-snippets >= 2.4.3+ , network-uri >= 2.6 && < 2.7+ , hakyll >= 4.6 && < 4.8+ , pandoc-types >=1.12 && <1.13+ , pandoc >= 1.13 && < 1.16+ , filepath >= 1.3 && < 1.5+ , directory >= 1.2 && < 1.3+ hs-source-dirs: src+ default-language: Haskell2010+ exposed-modules: Hakyll.Contrib.Agda++source-repository head+ type: git+ location: https://github.com/liamoc/agda-snippets
+ src/Hakyll/Contrib/Agda.hs view
@@ -0,0 +1,122 @@+{-# LANGUAGE LambdaCase #-}+module Hakyll.Contrib.Agda+ ( -- * Literate Agda Compilers+ literateAgdaCompiler+ , literateAgdaCompilerWith+ , literateAgdaCompilerWithTransform+ , literateAgdaCompilerWithTransformM+ -- * Building Blocks+ , defaultFileType+ , readLiterateAgda+ ) where+++import Agda.Contrib.Snippets+import Text.Pandoc.Options+import Text.Pandoc.Definition+import Hakyll.Core.Compiler+import Hakyll.Core.Item+import Hakyll.Core.Identifier+import Hakyll.Web.Pandoc+import Hakyll.Web.Pandoc.FileType+import System.FilePath+import System.Directory+import Network.URI+import Control.Exception++-- | Like 'literateAgdaCompilerWith', but an arbitrary transformation of the Pandoc+-- document can be added.+literateAgdaCompilerWithTransform+ :: CommandLineOptions -- ^ Agda command line options+ -> FileType -- ^ Format to use when reading other, non-Agda blocks.+ -> URI -- ^ Base URI where external libraries can be found.+ -> ReaderOptions -- ^ Pandoc reader options+ -> WriterOptions -- ^ Pandoc writer options+ -> (Item Pandoc -> Item Pandoc) -- ^ Transformation to run+ -> Compiler (Item String)+literateAgdaCompilerWithTransform opts ft uri ro wo+ = literateAgdaCompilerWithTransformM opts ft uri ro wo . (return .)++-- | Like 'literateAgdaCompiler', but Pandoc options can be specified.+literateAgdaCompilerWith+ :: CommandLineOptions -- ^ Agda command line options+ -> FileType -- ^ Format to use when reading other, non-Agda blocks.+ -> URI -- ^ Base URI where external libraries can be found.+ -> ReaderOptions -- ^ Pandoc reader options+ -> WriterOptions -- ^ Pandoc writer options+ -> Compiler (Item String)+literateAgdaCompilerWith opts ft uri ro wo+ = literateAgdaCompilerWithTransform opts ft uri ro wo id++-- | Compile a literate Agda document with the given Agda command line options,+-- text block format type, and library uri for hyperlinks.+literateAgdaCompiler+ :: CommandLineOptions -- ^ Agda command line options+ -> FileType -- ^ Format to use when reading other, non-Agda blocks.+ -> URI -- ^ Base URI where external libraries can be found.+ -> Compiler (Item String)+literateAgdaCompiler opts ft uri+ = literateAgdaCompilerWith opts ft uri defaultHakyllReaderOptions defaultHakyllWriterOptions++-- | Like 'literateAgdaCompilerWithTransform', but the transformation given is monadic.+literateAgdaCompilerWithTransformM+ :: CommandLineOptions -- ^ Agda command line options+ -> FileType -- ^ Format to use when reading other, non-Agda blocks.+ -> URI -- ^ Base URI where external libraries can be found.+ -> ReaderOptions -- ^ Pandoc reader options+ -> WriterOptions -- ^ Pandoc writer options+ -> (Item Pandoc -> Compiler (Item Pandoc)) -- ^ Transformation to run+ -> Compiler (Item String)+literateAgdaCompilerWithTransformM opts ft uri ro wo transform =+ fmap (writePandocWith wo) $ getResourceBody+ >>= readLiterateAgda opts uri+ >>= defaultFileType ft (readPandocWith ro)+ >>= transform++-- | Run a function that might be part of your compiler pipeline, except that if the+-- text format type cannot be detected from the extension (e.g, if it's a @lagda@ file),+-- the specified file type will be used instead of 'Binary'.+defaultFileType :: FileType -- ^ File type to default to+ -> (Item a -> Compiler (Item b)) -- ^ Pipeline function to run+ -> Item a+ -> Compiler (Item b)+defaultFileType t act i = do+ let tau Binary = t+ tau x = x+ x <- act (i {itemIdentifier = fromFilePath $ fn -<.> extensionFor (tau $ fileType fn) })+ return $ x {itemIdentifier = fromFilePath fn }+ where+ fn = toFilePath $ itemIdentifier i+ extensionFor = \case+ Binary -> takeExtension fn+ Css -> "css"+ DocBook -> "dbk"+ Html -> "html"+ LaTeX -> "tex"+ (LiterateHaskell f) -> extensionFor f ++ ".lhs"+ Markdown -> "md"+ MediaWiki -> "mediawiki"+ OrgMode -> "org"+ PlainText -> "txt"+ Rst -> "rst"+ Textile -> "textile"++-- | Read a literate Agda document using the given options, producing a string with+-- literate Agda snippets replaced with HTML, but everything else untouched.+readLiterateAgda :: CommandLineOptions -- ^ Agda command line options+ -> URI -- ^ Base URI where external libraries can be found.+ -> Item String+ -> Compiler (Item String)+readLiterateAgda aopt liburi i =+ if isAgda i+ then cached cacheName $+ do fp <- getResourceFilePath+ unsafeCompiler $ bracket getCurrentDirectory setCurrentDirectory $ const $+ do abfp <- canonicalizePath fp+ setCurrentDirectory (dropFileName abfp)+ s <- renderAgdaSnippets aopt "Agda" liburi abfp+ return $ i {itemBody = s}+ else return i+ where+ cacheName = "LiterateAgda.agdaCompiler"+ isAgda = (== ".lagda") . takeExtension . toFilePath . itemIdentifier