diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,31 @@ +Copyright Péter Diviánszky 2013 + +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 the copyright holder 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/PandocAgda.cabal b/PandocAgda.cabal new file mode 100644 --- /dev/null +++ b/PandocAgda.cabal @@ -0,0 +1,112 @@ +name: PandocAgda +version: 2.3.3 +cabal-version: >= 1.8 +build-type: Simple +license: BSD3 +license-file: LICENSE +author: Péter Diviánszky +maintainer: Péter Diviánszky +category: Dependent types +synopsis: Pandoc support for literate Agda +description: + Agda is a dependently typed functional programming language + and a proof assistant. + . + This package contains a modified Agda compiler which + process comments in literate Agda files with Pandoc. + Pandoc is a universal document converter. +tested-with: GHC == 7.6.1 +extra-source-files: src/full/Agda/undefined.h +data-dir: src/data +data-files: Agda.template + Agda.css + +source-repository head + type: darcs + location: http://code.haskell.org/Agda/ + +library + hs-source-dirs: src/full + + if os(windows) + build-depends: Win32 == 2.2.* + + build-depends: Agda == 2.3.3, + base >= 4.2 && < 4.7, + -- mtl-2.1 contains a severe bug + mtl >= 2.0 && < 2.1 || >= 2.1.1 && < 2.2, + QuickCheck >= 2.3 && < 2.6, + -- haskell-src-exts >= 1.9.6 && < 1.14, + containers >= 0.1 && < 0.6, + -- unordered-containers == 0.2.*, + -- pretty >= 1.0 && < 1.2, + -- bytestring >= 0.9.0.1 && < 0.11, + -- array >= 0.1 && < 0.5, + -- binary >= 0.4.4 && < 0.6, + -- zlib >= 0.4.0.1 && < 0.6, + filepath >= 1.1 && < 1.4, + -- process >= 1.0.1.0 && < 1.2, + -- haskeline >= 0.6.3.2 && < 0.8, + xhtml == 3000.2.*, + -- hashable >= 1.1.2.3 && < 1.3, + -- hashtables == 1.0.*, + -- geniplate >= 0.6.0.3 && < 0.7, + -- parallel < 3.3, + -- deepseq == 1.3.*, + pandoc == 1.10.*, + pandoc-types == 1.10.*, + text == 0.11.* + + if impl(ghc < 7.6) + build-depends: old-time >= 1.0 && < 1.2, + directory >= 1.0 && < 1.2 + else + build-depends: time == 1.4.*, + directory == 1.2.* + + extensions: CPP + exposed-modules: Agda.PandocMain + Agda.Interaction.Highlighting.PandocHTML + Agda.Interaction.PandocOptions + Agda.Interaction.PandocConvertOptions + other-modules: Paths_PandocAgda + if true + ghc-options: -w + -fwarn-deprecated-flags + -fwarn-dodgy-foreign-imports + -fwarn-dodgy-imports + -fwarn-duplicate-exports + -fwarn-hi-shadowing + -fwarn-incomplete-patterns + -fwarn-missing-fields + -fwarn-missing-methods + -fwarn-overlapping-patterns + -fwarn-warnings-deprecations + -- The Cabal-generated module Paths_Agda triggers a warning under + -- GHC 7.2.1/7.2.2 (at least when certain versions of Cabal are + -- used). + if impl(ghc < 7.2.1) || impl(ghc > 7.2.2) + ghc-options: -Werror + if impl(ghc >= 6.12) + ghc-options: -fwarn-dodgy-exports + -fwarn-wrong-do-bind + if impl(ghc >= 7.2) + ghc-options: -fwarn-identities + ghc-prof-options: -auto-all + +executable agdapandoc + hs-source-dirs: src/main + main-is: Main.hs + build-depends: PandocAgda == 2.3.3, + -- Nothing is used from the following package, except + -- for the prelude. + base >= 3 && < 6 + if impl(ghc >= 7) + -- If someone installs Agda with the setuid bit set, then the + -- presence of +RTS may be a security problem (see GHC bug #3910). + -- However, we sometimes recommend people to use +RTS to control + -- Agda's memory usage, so we want this functionality enabled by + -- default. + ghc-options: -rtsopts + + 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/src/data/Agda.css b/src/data/Agda.css new file mode 100644 --- /dev/null +++ b/src/data/Agda.css @@ -0,0 +1,33 @@ +/* Aspects. */ +.Comment { color: #B22222 } +.Keyword { color: #CD6600 } +.String { color: #B22222 } +.Number { color: #A020F0 } +.Symbol { color: #404040 } +.PrimitiveType { color: #0000CD } +.Operator {} + +/* NameKinds. */ +.Bound { color: black } +.InductiveConstructor { color: #008B00 } +.CoinductiveConstructor { color: #8B7500 } +.Datatype { color: #0000CD } +.Field { color: #EE1289 } +.Function { color: #0000CD } +.Module { color: #A020F0 } +.Postulate { color: #0000CD } +.Primitive { color: #0000CD } +.Record { color: #0000CD } + +/* OtherAspects. */ +.DottedPattern {} +.UnsolvedMeta { color: black; background: yellow } +.UnsolvedConstraint { color: black; background: yellow } +.TerminationProblem { color: black; background: #FFA07A } +.IncompletePattern { color: black; background: #F5DEB3 } +.Error { color: red; text-decoration: underline } +.TypeChecks { color: black; background: #ADD8E6 } + +/* Standard attributes. */ +a { text-decoration: none } +a[href]:hover { background-color: #B4EEB4 } diff --git a/src/data/Agda.template b/src/data/Agda.template new file mode 100644 --- /dev/null +++ b/src/data/Agda.template @@ -0,0 +1,58 @@ + + + + + + +$for(author-meta)$ + +$endfor$ +$if(date-meta)$ + +$endif$ + $if(title-prefix)$$title-prefix$ - $endif$$pagetitle$ + +$if(quotes)$ + +$endif$ +$if(highlighting-css)$ + +$endif$ +$for(css)$ + +$endfor$ +$if(math)$ + $math$ +$endif$ +$for(header-includes)$ + $header-includes$ +$endfor$ + + +$for(include-before)$ +$include-before$ +$endfor$ +$if(title)$ +
+

$title$

+$for(author)$ +

$author$

+$endfor$ +$if(date)$ +

$date$

+$endif$ +
+$endif$ +$if(toc)$ +
+$toc$ +
+$endif$ +$body$ +$for(include-after)$ +$include-after$ +$endfor$ + + diff --git a/src/full/Agda/Interaction/Highlighting/PandocHTML.hs b/src/full/Agda/Interaction/Highlighting/PandocHTML.hs new file mode 100644 --- /dev/null +++ b/src/full/Agda/Interaction/Highlighting/PandocHTML.hs @@ -0,0 +1,288 @@ +{-# LANGUAGE CPP #-} + +-- | Function for generating highlighted, hyperlinked HTML from Agda +-- sources. + +module Agda.Interaction.Highlighting.PandocHTML + ( generateHTML + ) where + +import Control.Applicative +import Control.Monad +import Control.Monad.Trans +import Control.Monad.State.Class +import Control.Arrow ((***)) +import System.FilePath +import System.Directory +import Text.XHtml.Strict +import Data.Function +import Data.Monoid +import Data.Maybe +import qualified Data.Map as Map +import qualified Data.List as List +import qualified Data.Char as Char + +import Text.Pandoc.Definition +import qualified Text.Pandoc.Definition as Pandoc +import Text.Pandoc.Options +import Text.Pandoc.Readers.Markdown +import Text.Pandoc.Writers.HTML + +import Paths_PandocAgda + +import Agda.Interaction.FindFile +import Agda.Interaction.Highlighting.Generate +import Agda.Interaction.Highlighting.Precise +import Agda.Interaction.Highlighting.Range +import Agda.TypeChecking.Monad (TCM) +import qualified Agda.TypeChecking.Monad as TCM +import qualified Agda.Syntax.Abstract as A +import qualified Agda.Syntax.Concrete as C +import Agda.Syntax.Common +import qualified Agda.Syntax.Scope.Monad as Scope +import Agda.Syntax.Translation.ConcreteToAbstract +import Agda.Interaction.Options +import qualified Agda.Interaction.PandocOptions as PO +import Agda.Utils.FileName (filePath) +import qualified Agda.Utils.IO.UTF8 as UTF8 +import Agda.Utils.Pretty + +import Agda.Utils.Impossible +#include "../../undefined.h" + +-- | The name of the default CSS file. + +defaultCSSFile :: FilePath +defaultCSSFile = "Agda.css" + +-- | The name of the default template file for pandoc. + +defaultTemplateFile :: FilePath +defaultTemplateFile = "Agda.template" + +-- | Generates HTML files from all the sources which the given module +-- depends on (including the module itself). +-- +-- This function should only be called after type checking has +-- completed successfully. + +generateHTML :: PO.CommandLineOptions -> A.ModuleName -> TCM () +generateHTML fullopts mod = do + options <- TCM.commandLineOptions + + -- There is a default directory given by 'defaultHTMLDir' + let dir = optHTMLDir options + liftIO $ createDirectoryIfMissing True dir + + -- If the default CSS file should be used, then it is copied to + -- the output directory. + liftIO $ when (isNothing $ optCSSFile options) $ do + cssFile <- getDataFileName defaultCSSFile + copyFile cssFile (dir defaultCSSFile) + + TCM.reportSLn "html" 1 $ unlines + [ "" + , "Warning: HTML is currently generated for ALL files which can be" + , "reached from the given module, including library files." + ] + + -- Pull highlighting info from the state and generate all the + -- web pages. + mapM_ (\(m, h) -> generatePage fullopts dir m h) =<< + map (id *** TCM.iHighlighting . TCM.miInterface) . + Map.toList <$> TCM.getVisitedModules + +-- | Converts module names to the corresponding HTML file names. + +modToFile :: C.TopLevelModuleName -> FilePath +modToFile m = render (pretty m) <.> "html" + +-- | Generates an HTML file with a highlighted, hyperlinked version of +-- the given module. + +generatePage + :: PO.CommandLineOptions + -> FilePath -- ^ Directory in which to create files. + -> C.TopLevelModuleName -- ^ Module to be highlighted. + -> HighlightingInfo -- ^ Syntax highlighting info for the module. + -> TCM () +generatePage fullopts dir mod highlighting = do + mf <- Map.lookup mod . TCM.stModuleToSource <$> get + case mf of + Nothing -> __IMPOSSIBLE__ + Just f -> do + contents <- liftIO $ UTF8.readTextFile $ filePath f + css <- maybe defaultCSSFile id . optCSSFile <$> + TCM.commandLineOptions + let mSlideVariant = fmap read $ PO.optGenerateHTML fullopts + html <- case mSlideVariant of + Just slideVariant | isLiterate (filePath f) -> do + templateFile <- maybe (liftIO $ getDataFileName defaultTemplateFile) return + (PO.optTemplateFile fullopts) + template <- liftIO $ UTF8.readTextFile templateFile + return $ pandocPage template css slideVariant mod contents highlighting + _ -> do + return $ renderHtml $ page css mod contents highlighting + TCM.reportSLn "html" 1 $ "Generating HTML for " ++ + render (pretty mod) ++ + " (" ++ target ++ ")." + liftIO $ UTF8.writeFile target html + where target = dir modToFile mod + + +-- | Constructs the web page, including headers. + +page :: FilePath -- ^ URL to the CSS file. + -> C.TopLevelModuleName -- ^ Module to be highlighted. + -> String -- ^ The contents of the module. + -> CompressedFile -- ^ Highlighting information. + -> Html +page css modName contents info = + header (thetitle << render (pretty modName) + +++ + meta ! [ httpequiv "Content-Type" + , content "text/html; charset=UTF-8" + ] + +++ + meta ! [ httpequiv "Content-Style-Type" + , content "text/css" + ] + +++ + thelink noHtml ! [ href css + , rel "stylesheet" + , thetype "text/css" + ]) + +++ + body << pre << code contents info + +--- | Constructs the HTML displaying the code. + +code :: String -- ^ The contents of the module. + -> CompressedFile -- ^ Highlighting information. + -> Html +code contents info = + mconcat $ + map (\(pos, s, mi) -> annotate pos mi (stringToHtml s)) $ + tokenStream contents info + +-- | Constructs the web page, including headers, with pandoc. + +pandocPage + :: String -- ^ Template + -> FilePath -- ^ URL to the CSS file. + -> HTMLSlideVariant -- ^ Slide variant + -> C.TopLevelModuleName -- ^ Module to be highlighted. + -> String -- ^ The contents of the module. + -> CompressedFile -- ^ Highlighting information. + -> String +pandocPage template css slideVariant modName contents info = + writeHtmlString def { writerStandalone = True + , writerTemplate = template + , writerTableOfContents = True + , writerSlideVariant = slideVariant + , writerVariables = [("css",css)] + } + $ Pandoc meta $ concat $ zipWith ($) (removeCodeBlocks md []) cf + where + cf = (++ [[]]) + . map conv + . getCode + . splitComment "\n\\begin{code}" + . splitComment "\n\\end{code}" + $ tokenStream contents info + + (Pandoc meta md) = readMarkdown def contents + + conv x = [Para [ RawInline "html" + . renderHtmlFragment + . (pre <<) + . mconcat + . map (\(pos, s, mi) -> annotate pos mi (stringToHtml s)) + $ x + ]] + + getCode ((_,s,_):xs) + | s == "\n\\begin{code}" || List.isPrefixOf "\\begin{code}" s + = getCode' xs [] + getCode (_:xs) = getCode xs + getCode [] = [] + + getCode' ((_,s,_):xs) + | s == "\n\\end{code}" || List.isPrefixOf "\\end{code}" s + = (: getCode xs) . reverse + getCode' (x:xs) = getCode' xs . (x:) + getCode' [] = error "__IMPOSSIBLE__" -- ??? + + splitComment w = concatMap f + where + f (pos, s, mi) = [(pos, t, mi) | t <- filter (not . null) $ g s []] + + g s | List.isPrefixOf w s = (: (w : g (drop (length w) s) [])) . reverse + g [] = (:[]) . reverse + g (c:cs) = g cs . (c:) + + removeCodeBlocks (RawBlock "latex" s: xs) | List.isPrefixOf "\\begin{code}" s + = removeCodeBlocks' (++) xs + removeCodeBlocks (RawBlock "html" s: xs) | List.isPrefixOf "