diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/agda-snippets-hakyll.cabal b/agda-snippets-hakyll.cabal new file mode 100644 --- /dev/null +++ b/agda-snippets-hakyll.cabal @@ -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 diff --git a/src/Hakyll/Contrib/Agda.hs b/src/Hakyll/Contrib/Agda.hs new file mode 100644 --- /dev/null +++ b/src/Hakyll/Contrib/Agda.hs @@ -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