{-# LANGUAGE ViewPatterns #-}
module Hakyll.Web.Agda
( markdownAgda
, pandocAgdaCompilerWith
, pandocAgdaCompiler
, isAgda
, agdaPandocCompiler
) where
import Agda.Interaction.FindFile (findFile, SourceFile(..))
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 Control.Monad.Except (catchError, throwError)
import Control.Monad.IO.Class (liftIO)
import Data.Char (isSpace)
import Data.Function (on)
import qualified Data.IntMap as IntMap
import Data.List (groupBy, isInfixOf, isPrefixOf, tails)
import Data.Maybe (fromMaybe)
import qualified Data.Set as Set
import Data.Text.Lazy (Text)
import qualified Data.Text.Lazy as TL
import Hakyll.Core.Compiler
import Hakyll.Core.Identifier
import Hakyll.Core.Item
import Hakyll.Web.Pandoc
import System.Directory (getCurrentDirectory, setCurrentDirectory, canonicalizePath, setCurrentDirectory)
import System.Exit (exitFailure)
import System.FilePath (dropFileName, splitExtension)
import Text.Pandoc (readMarkdown, ReaderOptions, WriterOptions)
import qualified Text.Pandoc as Pandoc
import Text.XHtml.Strict
import qualified Data.Text as T
checkFile :: SourceFile -> TCM TopLevelModuleName
checkFile :: SourceFile -> TCM TopLevelModuleName
checkFile SourceFile
file = do
TCM ()
TCM.resetState
SourceInfo
info <- SourceFile -> TCM SourceInfo
Imp.sourceInfo SourceFile
file
ModuleName -> TopLevelModuleName
toTopLevelModuleName (ModuleName -> TopLevelModuleName)
-> ((Interface, MaybeWarnings) -> ModuleName)
-> (Interface, MaybeWarnings)
-> TopLevelModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> ModuleName
TCM.iModuleName (Interface -> ModuleName)
-> ((Interface, MaybeWarnings) -> Interface)
-> (Interface, MaybeWarnings)
-> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Interface, MaybeWarnings) -> Interface
forall a b. (a, b) -> a
fst ((Interface, MaybeWarnings) -> TopLevelModuleName)
-> TCMT IO (Interface, MaybeWarnings) -> TCM TopLevelModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
SourceFile
-> Mode -> SourceInfo -> TCMT IO (Interface, MaybeWarnings)
Imp.typeCheckMain SourceFile
file Mode
Imp.TypeCheck SourceInfo
info
getModule :: TopLevelModuleName -> TCM (HighlightingInfo, Text)
getModule :: TopLevelModuleName -> TCM (HighlightingInfo, Text)
getModule TopLevelModuleName
m = do
Just ModuleInfo
mi <- TopLevelModuleName -> TCM (Maybe ModuleInfo)
TCM.getVisitedModule TopLevelModuleName
m
SourceFile
f <- TopLevelModuleName -> TCM SourceFile
findFile TopLevelModuleName
m
Text
s <- IO Text -> TCMT IO Text
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Text -> TCMT IO Text)
-> (SourceFile -> IO Text) -> SourceFile -> TCMT IO Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> IO Text
UTF8.readTextFile (FilePath -> IO Text)
-> (SourceFile -> FilePath) -> SourceFile -> IO Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> FilePath
filePath (AbsolutePath -> FilePath)
-> (SourceFile -> AbsolutePath) -> SourceFile -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceFile -> AbsolutePath
srcFilePath (SourceFile -> TCMT IO Text) -> SourceFile -> TCMT IO Text
forall a b. (a -> b) -> a -> b
$ SourceFile
f
(HighlightingInfo, Text) -> TCM (HighlightingInfo, Text)
forall (m :: * -> *) a. Monad m => a -> m a
return (Interface -> HighlightingInfo
TCM.iHighlighting (ModuleInfo -> Interface
TCM.miInterface ModuleInfo
mi), Text
s)
pairPositions :: HighlightingInfo -> String -> [(Integer, String, Aspects)]
pairPositions :: HighlightingInfo -> FilePath -> [(Integer, FilePath, Aspects)]
pairPositions HighlightingInfo
info FilePath
contents =
([(Maybe Aspects, (Key, Char))] -> (Integer, FilePath, Aspects))
-> [[(Maybe Aspects, (Key, Char))]]
-> [(Integer, FilePath, Aspects)]
forall a b. (a -> b) -> [a] -> [b]
map (\cs :: [(Maybe Aspects, (Key, Char))]
cs@((Maybe Aspects
mi, (Key
pos, Char
_)) : [(Maybe Aspects, (Key, Char))]
_) -> (Key -> Integer
forall a. Integral a => a -> Integer
toInteger Key
pos, ((Maybe Aspects, (Key, Char)) -> Char)
-> [(Maybe Aspects, (Key, Char))] -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map ((Key, Char) -> Char
forall a b. (a, b) -> b
snd ((Key, Char) -> Char)
-> ((Maybe Aspects, (Key, Char)) -> (Key, Char))
-> (Maybe Aspects, (Key, Char))
-> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Aspects, (Key, Char)) -> (Key, Char)
forall a b. (a, b) -> b
snd) [(Maybe Aspects, (Key, Char))]
cs, Aspects -> (Aspects -> Aspects) -> Maybe Aspects -> Aspects
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Aspects
forall a. Monoid a => a
mempty Aspects -> Aspects
forall a. a -> a
id Maybe Aspects
mi)) ([[(Maybe Aspects, (Key, Char))]]
-> [(Integer, FilePath, Aspects)])
-> [[(Maybe Aspects, (Key, Char))]]
-> [(Integer, FilePath, Aspects)]
forall a b. (a -> b) -> a -> b
$
((Maybe Aspects, (Key, Char))
-> (Maybe Aspects, (Key, Char)) -> Bool)
-> [(Maybe Aspects, (Key, Char))]
-> [[(Maybe Aspects, (Key, Char))]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (Maybe Aspects -> Maybe Aspects -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Maybe Aspects -> Maybe Aspects -> Bool)
-> ((Maybe Aspects, (Key, Char)) -> Maybe Aspects)
-> (Maybe Aspects, (Key, Char))
-> (Maybe Aspects, (Key, Char))
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Maybe Aspects, (Key, Char)) -> Maybe Aspects
forall a b. (a, b) -> a
fst) ([(Maybe Aspects, (Key, Char))]
-> [[(Maybe Aspects, (Key, Char))]])
-> [(Maybe Aspects, (Key, Char))]
-> [[(Maybe Aspects, (Key, Char))]]
forall a b. (a -> b) -> a -> b
$
((Key, Char) -> (Maybe Aspects, (Key, Char)))
-> [(Key, Char)] -> [(Maybe Aspects, (Key, Char))]
forall a b. (a -> b) -> [a] -> [b]
map (\(Key
pos, Char
c) -> (Key -> IntMap Aspects -> Maybe Aspects
forall a. Key -> IntMap a -> Maybe a
IntMap.lookup Key
pos IntMap Aspects
infoMap, (Key
pos, Char
c))) ([(Key, Char)] -> [(Maybe Aspects, (Key, Char))])
-> [(Key, Char)] -> [(Maybe Aspects, (Key, Char))]
forall a b. (a -> b) -> a -> b
$
[Key] -> FilePath -> [(Key, Char)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Key
1..] (FilePath -> [(Key, Char)]) -> FilePath -> [(Key, Char)]
forall a b. (a -> b) -> a -> b
$
FilePath
contents
where
infoMap :: IntMap Aspects
infoMap = File -> IntMap Aspects
toMap (HighlightingInfo -> File
decompress HighlightingInfo
info)
beginCode :: String -> Bool
beginCode :: FilePath -> Bool
beginCode FilePath
s = FilePath
"\\begin{code}" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` FilePath
s
endCode :: String -> Bool
endCode :: FilePath -> Bool
endCode FilePath
s = FilePath
"\\end{code}" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` FilePath
s
infixEnd :: Eq a => [a] -> [a] -> [a]
infixEnd :: [a] -> [a] -> [a]
infixEnd [a]
i [a]
s = [[a]] -> [a]
forall a. [a] -> a
head [Key -> [a] -> [a]
forall a. Key -> [a] -> [a]
drop ([a] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [a]
i) [a]
s' | [a]
s' <- [a] -> [[a]]
forall a. [a] -> [[a]]
tails [a]
s, [a]
i [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [a]
s']
stripBegin :: (Integer, String, Aspects) -> (Integer, String, Aspects)
stripBegin :: (Integer, FilePath, Aspects) -> (Integer, FilePath, Aspects)
stripBegin (Integer
i, FilePath
s, Aspects
mi) = (Integer
i, FilePath -> FilePath
cut ((Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
' ') (FilePath -> FilePath -> FilePath
forall a. Eq a => [a] -> [a] -> [a]
infixEnd FilePath
"\\begin{code}" FilePath
s)), Aspects
mi)
where
cut :: FilePath -> FilePath
cut (Char
'\n' : FilePath
s') = FilePath
s'
cut FilePath
s' = FilePath
s'
groupLiterate
:: [(Integer, String, Aspects)]
-> [Either String [(Integer, String, Aspects)]]
groupLiterate :: [(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
groupLiterate [(Integer, FilePath, Aspects)]
contents =
let ([(Integer, FilePath, Aspects)]
com, [(Integer, FilePath, Aspects)]
rest) = ((Integer, FilePath, Aspects) -> Bool)
-> [(Integer, FilePath, Aspects)]
-> ([(Integer, FilePath, Aspects)], [(Integer, FilePath, Aspects)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span ((FilePath -> Bool) -> (Integer, FilePath, Aspects) -> Bool
forall t a c. (t -> Bool) -> (a, t, c) -> Bool
notCode FilePath -> Bool
beginCode) [(Integer, FilePath, Aspects)]
contents
in FilePath -> Either FilePath [(Integer, FilePath, Aspects)]
forall a b. a -> Either a b
Left (FilePath
"\n\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [FilePath
s | (Integer
_, FilePath
s, Aspects
_) <- [(Integer, FilePath, Aspects)]
com] FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n\n") Either FilePath [(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
forall a. a -> [a] -> [a]
: [(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
go [(Integer, FilePath, Aspects)]
rest
where
go :: [(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
go [] = []
go ((Integer, FilePath, Aspects)
be : [(Integer, FilePath, Aspects)]
mis) =
let be' :: (Integer, FilePath, Aspects)
be'@(Integer
_, FilePath
s, Aspects
_) = (Integer, FilePath, Aspects) -> (Integer, FilePath, Aspects)
stripBegin (Integer, FilePath, Aspects)
be
([(Integer, FilePath, Aspects)]
code, [(Integer, FilePath, Aspects)]
rest) = ((Integer, FilePath, Aspects) -> Bool)
-> [(Integer, FilePath, Aspects)]
-> ([(Integer, FilePath, Aspects)], [(Integer, FilePath, Aspects)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span ((FilePath -> Bool) -> (Integer, FilePath, Aspects) -> Bool
forall t a c. (t -> Bool) -> (a, t, c) -> Bool
notCode FilePath -> Bool
endCode) [(Integer, FilePath, Aspects)]
mis
in if FilePath
"\\end{code}" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` FilePath
s
then
[(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
groupLiterate [(Integer, FilePath, Aspects)]
mis
else [(Integer, FilePath, Aspects)]
-> Either FilePath [(Integer, FilePath, Aspects)]
forall a b. b -> Either a b
Right ((Integer, FilePath, Aspects)
be' (Integer, FilePath, Aspects)
-> [(Integer, FilePath, Aspects)] -> [(Integer, FilePath, Aspects)]
forall a. a -> [a] -> [a]
: [(Integer, FilePath, Aspects)]
code) Either FilePath [(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
forall a. a -> [a] -> [a]
:
case [(Integer, FilePath, Aspects)]
rest of
[] -> FilePath -> [Either FilePath [(Integer, FilePath, Aspects)]]
forall a. HasCallStack => FilePath -> a
error FilePath
"malformed file"
((Integer
_, FilePath -> Bool
beginCode -> Bool
True, Aspects
_) : [(Integer, FilePath, Aspects)]
code') -> [(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
go [(Integer, FilePath, Aspects)]
code'
((Integer, FilePath, Aspects)
_ : [(Integer, FilePath, Aspects)]
com ) -> [(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
groupLiterate [(Integer, FilePath, Aspects)]
com
notCode :: (t -> Bool) -> (a, t, c) -> Bool
notCode t -> Bool
f (a
_, t
s, c
_) = Bool -> Bool
not (t -> Bool
f t
s)
annotate :: TopLevelModuleName -> Integer -> Aspects -> Html -> Html
annotate :: TopLevelModuleName -> Integer -> Aspects -> Html -> Html
annotate TopLevelModuleName
m Integer
pos Aspects
mi = Html -> Html
anchor (Html -> Html) -> [HtmlAttr] -> Html -> Html
forall a. ADDATTRS a => a -> [HtmlAttr] -> a
! [HtmlAttr]
attributes
where
attributes :: [HtmlAttr]
attributes = [FilePath -> HtmlAttr
name (Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
pos)] [HtmlAttr] -> [HtmlAttr] -> [HtmlAttr]
forall a. [a] -> [a] -> [a]
++
[HtmlAttr] -> Maybe [HtmlAttr] -> [HtmlAttr]
forall a. a -> Maybe a -> a
fromMaybe [] (Aspects -> Maybe DefinitionSite
definitionSite Aspects
mi Maybe DefinitionSite
-> (DefinitionSite -> Maybe [HtmlAttr]) -> Maybe [HtmlAttr]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= DefinitionSite -> Maybe [HtmlAttr]
link) [HtmlAttr] -> [HtmlAttr] -> [HtmlAttr]
forall a. [a] -> [a] -> [a]
++
(case [FilePath]
classes of [] -> []; [FilePath]
cs -> [FilePath -> HtmlAttr
theclass ([FilePath] -> FilePath
unwords [FilePath]
cs)])
classes :: [FilePath]
classes = [FilePath]
-> (FilePath -> [FilePath]) -> Maybe FilePath -> [FilePath]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] FilePath -> [FilePath]
forall p a. p -> [a]
noteClasses (Aspects -> Maybe FilePath
note Aspects
mi) [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++
Set OtherAspect -> [FilePath]
otherAspectClasses (Aspects -> Set OtherAspect
otherAspects Aspects
mi) [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++
[FilePath] -> (Aspect -> [FilePath]) -> Maybe Aspect -> [FilePath]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Aspect -> [FilePath]
aspectClasses (Aspects -> Maybe Aspect
aspect Aspects
mi)
aspectClasses :: Aspect -> [FilePath]
aspectClasses (Name Maybe NameKind
mKind Bool
op) =
let kindClass :: [FilePath]
kindClass = [FilePath]
-> (NameKind -> [FilePath]) -> Maybe NameKind -> [FilePath]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ((FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: []) (FilePath -> [FilePath])
-> (NameKind -> FilePath) -> NameKind -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameKind -> FilePath
showKind) Maybe NameKind
mKind
showKind :: NameKind -> FilePath
showKind (Constructor Induction
Inductive) = FilePath
"InductiveConstructor"
showKind (Constructor Induction
CoInductive) = FilePath
"CoinductiveConstructor"
showKind NameKind
k = NameKind -> FilePath
forall a. Show a => a -> FilePath
show NameKind
k
opClass :: [FilePath]
opClass = if Bool
op then [FilePath
"Operator"] else []
in [FilePath]
kindClass [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath]
opClass
aspectClasses Aspect
a = [Aspect -> FilePath
forall a. Show a => a -> FilePath
show Aspect
a]
otherAspectClasses :: Set OtherAspect -> [FilePath]
otherAspectClasses = (OtherAspect -> FilePath) -> [OtherAspect] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map OtherAspect -> FilePath
forall a. Show a => a -> FilePath
show ([OtherAspect] -> [FilePath])
-> (Set OtherAspect -> [OtherAspect])
-> Set OtherAspect
-> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set OtherAspect -> [OtherAspect]
forall a. Set a -> [a]
Set.toList
noteClasses :: p -> [a]
noteClasses p
_ = []
link :: DefinitionSite -> Maybe [HtmlAttr]
link DefinitionSite
defSite = if DefinitionSite -> TopLevelModuleName
defSiteModule DefinitionSite
defSite TopLevelModuleName -> TopLevelModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== TopLevelModuleName
m
then [HtmlAttr] -> Maybe [HtmlAttr]
forall a. a -> Maybe a
Just [FilePath -> HtmlAttr
href (FilePath
"#" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Key -> FilePath
forall a. Show a => a -> FilePath
show (DefinitionSite -> Key
defSitePos DefinitionSite
defSite))]
else Maybe [HtmlAttr]
forall a. Maybe a
Nothing
toMarkdown :: String
-> TopLevelModuleName -> [Either String [(Integer, String, Aspects)]]
-> String
toMarkdown :: FilePath
-> TopLevelModuleName
-> [Either FilePath [(Integer, FilePath, Aspects)]]
-> FilePath
toMarkdown FilePath
classpr TopLevelModuleName
m [Either FilePath [(Integer, FilePath, Aspects)]]
contents =
[FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ case Either FilePath [(Integer, FilePath, Aspects)]
c of
Left FilePath
s -> FilePath
s
Right [(Integer, FilePath, Aspects)]
cs ->
let h :: Html
h = Html -> Html
pre (Html -> Html) -> ([Html] -> Html) -> [Html] -> Html
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Html -> Html
tag FilePath
"code" (Html -> Html) -> ([Html] -> Html) -> [Html] -> Html
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Html] -> Html
forall a. Monoid a => [a] -> a
mconcat ([Html] -> Html) -> [Html] -> Html
forall a b. (a -> b) -> a -> b
$
[ (TopLevelModuleName -> Integer -> Aspects -> Html -> Html
annotate TopLevelModuleName
m Integer
pos Aspects
mi (FilePath -> Html
stringToHtml FilePath
s))
| (Integer
pos, FilePath
s, Aspects
mi) <- [(Integer, FilePath, Aspects)]
cs ]
in Html -> FilePath
forall html. HTML html => html -> FilePath
renderHtmlFragment (Html
h Html -> [HtmlAttr] -> Html
forall a. ADDATTRS a => a -> [HtmlAttr] -> a
! [FilePath -> HtmlAttr
theclass FilePath
classpr])
| Either FilePath [(Integer, FilePath, Aspects)]
c <- [Either FilePath [(Integer, FilePath, Aspects)]]
contents ]
convert :: String -> TopLevelModuleName -> TCM String
convert :: FilePath -> TopLevelModuleName -> TCM FilePath
convert FilePath
classpr TopLevelModuleName
m =
do (HighlightingInfo
info, Text
contents) <- TopLevelModuleName -> TCM (HighlightingInfo, Text)
getModule TopLevelModuleName
m
FilePath -> TCM FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> TCM FilePath)
-> (Text -> FilePath) -> Text -> TCM FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath
-> TopLevelModuleName
-> [Either FilePath [(Integer, FilePath, Aspects)]]
-> FilePath
toMarkdown FilePath
classpr TopLevelModuleName
m ([Either FilePath [(Integer, FilePath, Aspects)]] -> FilePath)
-> (Text -> [Either FilePath [(Integer, FilePath, Aspects)]])
-> Text
-> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]]
groupLiterate ([(Integer, FilePath, Aspects)]
-> [Either FilePath [(Integer, FilePath, Aspects)]])
-> (Text -> [(Integer, FilePath, Aspects)])
-> Text
-> [Either FilePath [(Integer, FilePath, Aspects)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HighlightingInfo -> FilePath -> [(Integer, FilePath, Aspects)]
pairPositions HighlightingInfo
info (FilePath -> [(Integer, FilePath, Aspects)])
-> (Text -> FilePath) -> Text -> [(Integer, FilePath, Aspects)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
TL.unpack (Text -> TCM FilePath) -> Text -> TCM FilePath
forall a b. (a -> b) -> a -> b
$ Text
contents
markdownAgda :: CommandLineOptions -> String -> SourceFile -> IO String
markdownAgda :: CommandLineOptions -> FilePath -> SourceFile -> IO FilePath
markdownAgda CommandLineOptions
opts FilePath
classpr SourceFile
file =
do let check :: TCM FilePath
check = do
CommandLineOptions -> TCM ()
TCM.setCommandLineOptions CommandLineOptions
opts
SourceFile -> TCM TopLevelModuleName
checkFile SourceFile
file TCM TopLevelModuleName
-> (TopLevelModuleName -> TCM FilePath) -> TCM FilePath
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FilePath -> TopLevelModuleName -> TCM FilePath
convert FilePath
classpr
Either TCErr FilePath
r <- TCM FilePath -> IO (Either TCErr FilePath)
forall a. TCM a -> IO (Either TCErr a)
TCM.runTCMTop (TCM FilePath -> IO (Either TCErr FilePath))
-> TCM FilePath -> IO (Either TCErr FilePath)
forall a b. (a -> b) -> a -> b
$ TCM FilePath
check TCM FilePath -> (TCErr -> TCM FilePath) -> TCM FilePath
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
err -> do
FilePath
s <- TCErr -> TCM FilePath
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm FilePath
prettyError TCErr
err
IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (FilePath -> IO ()
putStrLn FilePath
s)
TCErr -> TCM FilePath
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
case Either TCErr FilePath
r of
Right FilePath
s -> FilePath -> IO FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return ((Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace FilePath
s)
Left TCErr
_ -> IO FilePath
forall a. IO a
exitFailure
isAgda :: Item a -> Bool
isAgda :: Item a -> Bool
isAgda Item a
i = FilePath
ex FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
".lagda"
where
ex :: FilePath
ex = (FilePath, FilePath) -> FilePath
forall a b. (a, b) -> b
snd ((FilePath, FilePath) -> FilePath)
-> (Item a -> (FilePath, FilePath)) -> Item a -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> (FilePath, FilePath)
splitExtension (FilePath -> (FilePath, FilePath))
-> (Item a -> FilePath) -> Item a -> (FilePath, FilePath)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identifier -> FilePath
toFilePath (Identifier -> FilePath)
-> (Item a -> Identifier) -> Item a -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Item a -> Identifier
forall a. Item a -> Identifier
itemIdentifier (Item a -> FilePath) -> Item a -> FilePath
forall a b. (a -> b) -> a -> b
$ Item a
i
saveDir :: IO a -> IO a
saveDir :: IO a -> IO a
saveDir IO a
m = do
FilePath
origDir <- IO FilePath
getCurrentDirectory
IO a
m IO a -> IO () -> IO a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* FilePath -> IO ()
setCurrentDirectory FilePath
origDir
agdaPandocCompiler :: ReaderOptions -> WriterOptions -> CommandLineOptions -> Compiler (Item String)
agdaPandocCompiler :: ReaderOptions
-> WriterOptions -> CommandLineOptions -> Compiler (Item FilePath)
agdaPandocCompiler ReaderOptions
ropt WriterOptions
wopt CommandLineOptions
aopt = do
Item FilePath
i <- Compiler (Item FilePath)
getResourceBody
FilePath -> Compiler (Item FilePath) -> Compiler (Item FilePath)
forall a.
(Binary a, Typeable a) =>
FilePath -> Compiler a -> Compiler a
cached FilePath
cacheName (Compiler (Item FilePath) -> Compiler (Item FilePath))
-> Compiler (Item FilePath) -> Compiler (Item FilePath)
forall a b. (a -> b) -> a -> b
$ do
FilePath
fp <- Compiler FilePath
getResourceFilePath
IO (Item FilePath) -> Compiler (Item FilePath)
forall a. IO a -> Compiler a
unsafeCompiler (IO (Item FilePath) -> Compiler (Item FilePath))
-> IO (Item FilePath) -> Compiler (Item FilePath)
forall a b. (a -> b) -> a -> b
$ IO (Item FilePath) -> IO (Item FilePath)
forall a. IO a -> IO a
saveDir (IO (Item FilePath) -> IO (Item FilePath))
-> IO (Item FilePath) -> IO (Item FilePath)
forall a b. (a -> b) -> a -> b
$ do
FilePath
abfp <- FilePath -> IO FilePath
canonicalizePath FilePath
fp
FilePath -> IO ()
setCurrentDirectory (FilePath -> FilePath
dropFileName FilePath
abfp)
FilePath
s <- CommandLineOptions -> FilePath -> SourceFile -> IO FilePath
markdownAgda CommandLineOptions
aopt FilePath
"Agda" (AbsolutePath -> SourceFile
SourceFile (AbsolutePath -> SourceFile) -> AbsolutePath -> SourceFile
forall a b. (a -> b) -> a -> b
$ FilePath -> AbsolutePath
mkAbsolute FilePath
abfp)
let i' :: Item Text
i' = Item FilePath
i {itemBody :: Text
itemBody = FilePath -> Text
T.pack FilePath
s}
case PandocPure (Item Pandoc) -> Either PandocError (Item Pandoc)
forall a. PandocPure a -> Either PandocError a
Pandoc.runPure ((Text -> PandocPure Pandoc)
-> Item Text -> PandocPure (Item Pandoc)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (ReaderOptions -> Text -> PandocPure Pandoc
forall (m :: * -> *).
PandocMonad m =>
ReaderOptions -> Text -> m Pandoc
readMarkdown ReaderOptions
ropt) Item Text
i') of
Left PandocError
err -> FilePath -> IO (Item FilePath)
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> IO (Item FilePath)) -> FilePath -> IO (Item FilePath)
forall a b. (a -> b) -> a -> b
$ FilePath
"pandocAgdaCompilerWith: Pandoc failed with error " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ PandocError -> FilePath
forall a. Show a => a -> FilePath
show PandocError
err
Right Item Pandoc
i'' -> Item FilePath -> IO (Item FilePath)
forall (m :: * -> *) a. Monad m => a -> m a
return (Item FilePath -> IO (Item FilePath))
-> Item FilePath -> IO (Item FilePath)
forall a b. (a -> b) -> a -> b
$ WriterOptions -> Item Pandoc -> Item FilePath
writePandocWith WriterOptions
wopt Item Pandoc
i''
where
cacheName :: FilePath
cacheName = FilePath
"LiterateAgda.pandocAgdaCompilerWith"
pandocAgdaCompilerWith :: ReaderOptions -> WriterOptions -> CommandLineOptions
-> Compiler (Item String)
pandocAgdaCompilerWith :: ReaderOptions
-> WriterOptions -> CommandLineOptions -> Compiler (Item FilePath)
pandocAgdaCompilerWith ReaderOptions
ropt WriterOptions
wopt CommandLineOptions
aopt = do
Item FilePath
i <- Compiler (Item FilePath)
getResourceBody
if Item FilePath -> Bool
forall a. Item a -> Bool
isAgda Item FilePath
i
then ReaderOptions
-> WriterOptions -> CommandLineOptions -> Compiler (Item FilePath)
agdaPandocCompiler ReaderOptions
ropt WriterOptions
wopt CommandLineOptions
aopt
else ReaderOptions -> WriterOptions -> Compiler (Item FilePath)
pandocCompilerWith ReaderOptions
ropt WriterOptions
wopt
pandocAgdaCompiler :: Compiler (Item String)
pandocAgdaCompiler :: Compiler (Item FilePath)
pandocAgdaCompiler =
ReaderOptions
-> WriterOptions -> CommandLineOptions -> Compiler (Item FilePath)
pandocAgdaCompilerWith ReaderOptions
defaultHakyllReaderOptions WriterOptions
defaultHakyllWriterOptions
CommandLineOptions
defaultOptions