{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeApplications #-}
module Blagda
( module Blagda
, module Blagda.Template
, module Blagda.Types
, loadMarkdown
, rename
) where
import Blagda.Agda
import Blagda.Markdown
import Blagda.Template
import Blagda.Rename (rename)
import Blagda.Types
import Blagda.Utils (pattern Strs)
import Data.List
import Data.Map.Lazy (Map)
import Data.Text (Text)
import Development.Shake
import Development.Shake.FilePath
import Text.Pandoc
parseFileTypes :: () -> Action (Map Text Text)
parseFileTypes :: () -> Action (Map Text Text)
parseFileTypes () = do
Partial => [FilePath] -> Action ()
[FilePath] -> Action ()
need [FilePath
"_build/all-pages.agda"]
FilePath -> IO (Map Text Text) -> Action (Map Text Text)
forall a. FilePath -> IO a -> Action a
traced FilePath
"loading types from iface" (IO (Map Text Text) -> Action (Map Text Text))
-> ((FilePath -> TCMT IO (Map Text Text)) -> IO (Map Text Text))
-> (FilePath -> TCMT IO (Map Text Text))
-> Action (Map Text Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath -> TCMT IO (Map Text Text)) -> IO (Map Text Text)
forall a. (FilePath -> TCMT IO a) -> IO a
runAgda ((FilePath -> TCMT IO (Map Text Text)) -> Action (Map Text Text))
-> (FilePath -> TCMT IO (Map Text Text)) -> Action (Map Text Text)
forall a b. (a -> b) -> a -> b
$
FilePath -> FilePath -> TCMT IO (Map Text Text)
tcAndLoadPublicNames FilePath
"_build/all-pages.agda"
agdaHTML :: FilePath -> Action [FilePath]
agdaHTML :: FilePath -> Action [FilePath]
agdaHTML FilePath
dir = do
[FilePath]
agda_files <- [FilePath] -> [FilePath]
forall a. Ord a => [a] -> [a]
sort ([FilePath] -> [FilePath])
-> Action [FilePath] -> Action [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> [FilePath] -> Action [FilePath]
getDirectoryFiles FilePath
dir [FilePath
"**/*.agda", FilePath
"**/*.lagda.md"]
let
toOut :: FilePath -> FilePath
toOut FilePath
x | FilePath -> FilePath
takeExtensions FilePath
x FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
".lagda.md"
= FilePath -> FilePath
moduleName (FilePath -> FilePath
dropExtensions FilePath
x) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" -- (text page)"
toOut FilePath
x = FilePath -> FilePath
moduleName (FilePath -> FilePath
dropExtensions FilePath
x) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" -- (code only)"
FilePath -> [FilePath] -> Action ()
forall (m :: * -> *).
(MonadIO m, Partial) =>
FilePath -> [FilePath] -> m ()
writeFileLines FilePath
"_build/all-pages.agda"
([FilePath] -> Action ()) -> [FilePath] -> Action ()
forall a b. (a -> b) -> a -> b
$ [FilePath
"open import " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
toOut FilePath
x | FilePath
x <- [FilePath]
agda_files]
[FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath
"import " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
x FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" -- (builtin)" | FilePath
x <- [FilePath]
builtinModules]
[CmdOption] -> FilePath -> [FilePath] -> Action ()
forall r.
(Partial, CmdResult r) =>
[CmdOption] -> FilePath -> [FilePath] -> Action r
command @() [] FilePath
"agda"
[ FilePath
"--html"
, FilePath
"--html-dir=_build/html0"
, FilePath
"--html-highlight=auto"
, FilePath
"--local-interfaces"
, FilePath
"--css=/css/agda-cats.css"
, FilePath
"_build/all-pages.agda"
]
[FilePath] -> Action [FilePath]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [FilePath]
agda_files
parseMetaString :: MetaValue -> Maybe Text
parseMetaString :: MetaValue -> Maybe Text
parseMetaString (MetaString Text
txt) = Text -> Maybe Text
forall a. a -> Maybe a
Just Text
txt
parseMetaString (MetaInlines (Strs Text
txt)) = Text -> Maybe Text
forall a. a -> Maybe a
Just Text
txt
parseMetaString MetaValue
_ = Maybe Text
forall a. Maybe a
Nothing