{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Interaction.Highlighting.HTML.Backend
( htmlBackend
) where
import Agda.Interaction.Highlighting.HTML.Base
import Prelude hiding ((!!), concatMap)
import Control.DeepSeq
import Control.Monad.Trans ( MonadIO )
import Control.Monad.Except ( MonadError(throwError) )
import Data.Map (Map)
import GHC.Generics (Generic)
import Agda.Interaction.Options
( ArgDescr(ReqArg, NoArg)
, OptDescr(..)
, Flag
)
import Agda.Compiler.Backend (Backend,Backend_boot(..), Backend',Backend'_boot(..), Recompile(..))
import Agda.Compiler.Common (IsMain(..), curIF)
import Agda.Syntax.TopLevelModuleName (TopLevelModuleName)
import Agda.TypeChecking.Monad
( MonadDebug
, ReadTCState
, Definition
, reportS
)
data HtmlFlags = HtmlFlags
{ HtmlFlags -> Bool
htmlFlagEnabled :: Bool
, HtmlFlags -> String
htmlFlagDir :: FilePath
, HtmlFlags -> HtmlHighlight
htmlFlagHighlight :: HtmlHighlight
, HtmlFlags -> Bool
htmlFlagHighlightOccurrences :: Bool
, HtmlFlags -> Maybe String
htmlFlagCssFile :: Maybe FilePath
} deriving (HtmlFlags -> HtmlFlags -> Bool
(HtmlFlags -> HtmlFlags -> Bool)
-> (HtmlFlags -> HtmlFlags -> Bool) -> Eq HtmlFlags
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HtmlFlags -> HtmlFlags -> Bool
== :: HtmlFlags -> HtmlFlags -> Bool
$c/= :: HtmlFlags -> HtmlFlags -> Bool
/= :: HtmlFlags -> HtmlFlags -> Bool
Eq, (forall x. HtmlFlags -> Rep HtmlFlags x)
-> (forall x. Rep HtmlFlags x -> HtmlFlags) -> Generic HtmlFlags
forall x. Rep HtmlFlags x -> HtmlFlags
forall x. HtmlFlags -> Rep HtmlFlags x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. HtmlFlags -> Rep HtmlFlags x
from :: forall x. HtmlFlags -> Rep HtmlFlags x
$cto :: forall x. Rep HtmlFlags x -> HtmlFlags
to :: forall x. Rep HtmlFlags x -> HtmlFlags
Generic)
instance NFData HtmlFlags
data HtmlCompileEnv = HtmlCompileEnv
{ HtmlCompileEnv -> HtmlOptions
htmlCompileEnvOpts :: HtmlOptions
}
data HtmlModuleEnv = HtmlModuleEnv
{ HtmlModuleEnv -> HtmlCompileEnv
htmlModEnvCompileEnv :: HtmlCompileEnv
, HtmlModuleEnv -> TopLevelModuleName
htmlModEnvName :: TopLevelModuleName
}
data HtmlModule = HtmlModule
data HtmlDef = HtmlDef
htmlBackend :: Backend
htmlBackend :: Backend
htmlBackend = Backend'_boot
TCM HtmlFlags HtmlCompileEnv HtmlModuleEnv HtmlModule HtmlDef
-> Backend
forall opts (tcm :: * -> *) env menv mod def.
NFData opts =>
Backend'_boot tcm opts env menv mod def -> Backend_boot tcm
Backend Backend'_boot
TCM HtmlFlags HtmlCompileEnv HtmlModuleEnv HtmlModule HtmlDef
htmlBackend'
htmlBackend' :: Backend' HtmlFlags HtmlCompileEnv HtmlModuleEnv HtmlModule HtmlDef
htmlBackend' :: Backend'_boot
TCM HtmlFlags HtmlCompileEnv HtmlModuleEnv HtmlModule HtmlDef
htmlBackend' = Backend'
{ backendName :: String
backendName = String
"HTML"
, backendVersion :: Maybe String
backendVersion = Maybe String
forall a. Maybe a
Nothing
, options :: HtmlFlags
options = HtmlFlags
initialHtmlFlags
, commandLineFlags :: [OptDescr (Flag HtmlFlags)]
commandLineFlags = [OptDescr (Flag HtmlFlags)]
htmlFlags
, isEnabled :: HtmlFlags -> Bool
isEnabled = HtmlFlags -> Bool
htmlFlagEnabled
, preCompile :: HtmlFlags -> TCM HtmlCompileEnv
preCompile = HtmlFlags -> TCM HtmlCompileEnv
forall (m :: * -> *).
(MonadIO m, MonadDebug m) =>
HtmlFlags -> m HtmlCompileEnv
preCompileHtml
, preModule :: HtmlCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe String
-> TCM (Recompile HtmlModuleEnv HtmlModule)
preModule = HtmlCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe String
-> TCM (Recompile HtmlModuleEnv HtmlModule)
forall (m :: * -> *).
Applicative m =>
HtmlCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe String
-> m (Recompile HtmlModuleEnv HtmlModule)
preModuleHtml
, compileDef :: HtmlCompileEnv
-> HtmlModuleEnv -> IsMain -> Definition -> TCM HtmlDef
compileDef = HtmlCompileEnv
-> HtmlModuleEnv -> IsMain -> Definition -> TCM HtmlDef
forall (m :: * -> *).
Applicative m =>
HtmlCompileEnv
-> HtmlModuleEnv -> IsMain -> Definition -> m HtmlDef
compileDefHtml
, postModule :: HtmlCompileEnv
-> HtmlModuleEnv
-> IsMain
-> TopLevelModuleName
-> [HtmlDef]
-> TCM HtmlModule
postModule = HtmlCompileEnv
-> HtmlModuleEnv
-> IsMain
-> TopLevelModuleName
-> [HtmlDef]
-> TCM HtmlModule
forall (m :: * -> *).
(MonadIO m, MonadDebug m, ReadTCState m) =>
HtmlCompileEnv
-> HtmlModuleEnv
-> IsMain
-> TopLevelModuleName
-> [HtmlDef]
-> m HtmlModule
postModuleHtml
, postCompile :: HtmlCompileEnv
-> IsMain -> Map TopLevelModuleName HtmlModule -> TCM ()
postCompile = HtmlCompileEnv
-> IsMain -> Map TopLevelModuleName HtmlModule -> TCM ()
forall (m :: * -> *).
Applicative m =>
HtmlCompileEnv
-> IsMain -> Map TopLevelModuleName HtmlModule -> m ()
postCompileHtml
, scopeCheckingSuffices :: Bool
scopeCheckingSuffices = Bool
True
, mayEraseType :: QName -> TCM Bool
mayEraseType = TCM Bool -> QName -> TCM Bool
forall a b. a -> b -> a
const (TCM Bool -> QName -> TCM Bool) -> TCM Bool -> QName -> TCM Bool
forall a b. (a -> b) -> a -> b
$ Bool -> TCM Bool
forall a. a -> TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
}
initialHtmlFlags :: HtmlFlags
initialHtmlFlags :: HtmlFlags
initialHtmlFlags = HtmlFlags
{ htmlFlagEnabled :: Bool
htmlFlagEnabled = Bool
False
, htmlFlagDir :: String
htmlFlagDir = String
defaultHTMLDir
, htmlFlagHighlight :: HtmlHighlight
htmlFlagHighlight = HtmlHighlight
HighlightAll
, htmlFlagHighlightOccurrences :: Bool
htmlFlagHighlightOccurrences = Bool
False
, htmlFlagCssFile :: Maybe String
htmlFlagCssFile = Maybe String
forall a. Maybe a
Nothing
}
htmlOptsOfFlags :: HtmlFlags -> HtmlOptions
htmlOptsOfFlags :: HtmlFlags -> HtmlOptions
htmlOptsOfFlags HtmlFlags
flags = HtmlOptions
{ htmlOptDir :: String
htmlOptDir = HtmlFlags -> String
htmlFlagDir HtmlFlags
flags
, htmlOptHighlight :: HtmlHighlight
htmlOptHighlight = HtmlFlags -> HtmlHighlight
htmlFlagHighlight HtmlFlags
flags
, htmlOptHighlightOccurrences :: Bool
htmlOptHighlightOccurrences = HtmlFlags -> Bool
htmlFlagHighlightOccurrences HtmlFlags
flags
, htmlOptCssFile :: Maybe String
htmlOptCssFile = HtmlFlags -> Maybe String
htmlFlagCssFile HtmlFlags
flags
}
defaultHTMLDir :: FilePath
defaultHTMLDir :: String
defaultHTMLDir = String
"html"
htmlFlags :: [OptDescr (Flag HtmlFlags)]
htmlFlags :: [OptDescr (Flag HtmlFlags)]
htmlFlags =
[ String
-> [String]
-> ArgDescr (Flag HtmlFlags)
-> String
-> OptDescr (Flag HtmlFlags)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"html"] (Flag HtmlFlags -> ArgDescr (Flag HtmlFlags)
forall a. a -> ArgDescr a
NoArg Flag HtmlFlags
htmlFlag)
String
"generate HTML files with highlighted source code"
, String
-> [String]
-> ArgDescr (Flag HtmlFlags)
-> String
-> OptDescr (Flag HtmlFlags)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"html-dir"] ((String -> Flag HtmlFlags) -> String -> ArgDescr (Flag HtmlFlags)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag HtmlFlags
htmlDirFlag String
"DIR")
(String
"directory in which HTML files are placed (default: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
defaultHTMLDir String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")")
, String
-> [String]
-> ArgDescr (Flag HtmlFlags)
-> String
-> OptDescr (Flag HtmlFlags)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"highlight-occurrences"] (Flag HtmlFlags -> ArgDescr (Flag HtmlFlags)
forall a. a -> ArgDescr a
NoArg Flag HtmlFlags
highlightOccurrencesFlag)
(String
"highlight all occurrences of hovered symbol in generated " String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"HTML files")
, String
-> [String]
-> ArgDescr (Flag HtmlFlags)
-> String
-> OptDescr (Flag HtmlFlags)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"css"] ((String -> Flag HtmlFlags) -> String -> ArgDescr (Flag HtmlFlags)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag HtmlFlags
cssFlag String
"URL")
String
"the CSS file used by the HTML files (can be relative)"
, String
-> [String]
-> ArgDescr (Flag HtmlFlags)
-> String
-> OptDescr (Flag HtmlFlags)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"html-highlight"] ((String -> Flag HtmlFlags) -> String -> ArgDescr (Flag HtmlFlags)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag HtmlFlags
htmlHighlightFlag String
"[code,all,auto]")
(String
"whether to highlight only the code parts (code) or " String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"the file as a whole (all) or " String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"decide by source file type (auto)")
]
htmlFlag :: Flag HtmlFlags
htmlFlag :: Flag HtmlFlags
htmlFlag HtmlFlags
o = Flag HtmlFlags
forall a. a -> OptM a
forall (m :: * -> *) a. Monad m => a -> m a
return Flag HtmlFlags -> Flag HtmlFlags
forall a b. (a -> b) -> a -> b
$ HtmlFlags
o { htmlFlagEnabled = True }
htmlDirFlag :: FilePath -> Flag HtmlFlags
htmlDirFlag :: String -> Flag HtmlFlags
htmlDirFlag String
d HtmlFlags
o = Flag HtmlFlags
forall a. a -> OptM a
forall (m :: * -> *) a. Monad m => a -> m a
return Flag HtmlFlags -> Flag HtmlFlags
forall a b. (a -> b) -> a -> b
$ HtmlFlags
o { htmlFlagDir = d }
cssFlag :: FilePath -> Flag HtmlFlags
cssFlag :: String -> Flag HtmlFlags
cssFlag String
f HtmlFlags
o = Flag HtmlFlags
forall a. a -> OptM a
forall (m :: * -> *) a. Monad m => a -> m a
return Flag HtmlFlags -> Flag HtmlFlags
forall a b. (a -> b) -> a -> b
$ HtmlFlags
o { htmlFlagCssFile = Just f }
highlightOccurrencesFlag :: Flag HtmlFlags
highlightOccurrencesFlag :: Flag HtmlFlags
highlightOccurrencesFlag HtmlFlags
o = Flag HtmlFlags
forall a. a -> OptM a
forall (m :: * -> *) a. Monad m => a -> m a
return Flag HtmlFlags -> Flag HtmlFlags
forall a b. (a -> b) -> a -> b
$ HtmlFlags
o { htmlFlagHighlightOccurrences = True }
parseHtmlHighlightFlag :: MonadError String m => String -> m HtmlHighlight
parseHtmlHighlightFlag :: forall (m :: * -> *).
MonadError String m =>
String -> m HtmlHighlight
parseHtmlHighlightFlag String
"code" = HtmlHighlight -> m HtmlHighlight
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return HtmlHighlight
HighlightCode
parseHtmlHighlightFlag String
"all" = HtmlHighlight -> m HtmlHighlight
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return HtmlHighlight
HighlightAll
parseHtmlHighlightFlag String
"auto" = HtmlHighlight -> m HtmlHighlight
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return HtmlHighlight
HighlightAuto
parseHtmlHighlightFlag String
opt = String -> m HtmlHighlight
forall a. String -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> m HtmlHighlight) -> String -> m HtmlHighlight
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"Invalid option <", String
opt, String
">, expected <all>, <auto> or <code>"]
htmlHighlightFlag :: String -> Flag HtmlFlags
htmlHighlightFlag :: String -> Flag HtmlFlags
htmlHighlightFlag String
opt HtmlFlags
o = do
HtmlHighlight
flag <- String -> OptM HtmlHighlight
forall (m :: * -> *).
MonadError String m =>
String -> m HtmlHighlight
parseHtmlHighlightFlag String
opt
Flag HtmlFlags
forall a. a -> OptM a
forall (m :: * -> *) a. Monad m => a -> m a
return Flag HtmlFlags -> Flag HtmlFlags
forall a b. (a -> b) -> a -> b
$ HtmlFlags
o { htmlFlagHighlight = flag }
runLogHtmlWithMonadDebug :: MonadDebug m => LogHtmlT m a -> m a
runLogHtmlWithMonadDebug :: forall (m :: * -> *) a. MonadDebug m => LogHtmlT m a -> m a
runLogHtmlWithMonadDebug = HtmlLogAction m -> LogHtmlT m a -> m a
forall (m :: * -> *) a.
Monad m =>
HtmlLogAction m -> LogHtmlT m a -> m a
runLogHtmlWith (HtmlLogAction m -> LogHtmlT m a -> m a)
-> HtmlLogAction m -> LogHtmlT m a -> m a
forall a b. (a -> b) -> a -> b
$ String -> VerboseLevel -> HtmlLogAction m
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> VerboseLevel -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportS String
"html" VerboseLevel
1
preCompileHtml
:: (MonadIO m, MonadDebug m)
=> HtmlFlags
-> m HtmlCompileEnv
preCompileHtml :: forall (m :: * -> *).
(MonadIO m, MonadDebug m) =>
HtmlFlags -> m HtmlCompileEnv
preCompileHtml HtmlFlags
flags = LogHtmlT m HtmlCompileEnv -> m HtmlCompileEnv
forall (m :: * -> *) a. MonadDebug m => LogHtmlT m a -> m a
runLogHtmlWithMonadDebug (LogHtmlT m HtmlCompileEnv -> m HtmlCompileEnv)
-> LogHtmlT m HtmlCompileEnv -> m HtmlCompileEnv
forall a b. (a -> b) -> a -> b
$ do
HtmlLogAction (ReaderT (HtmlLogAction m) m)
forall (m :: * -> *). MonadLogHtml m => HtmlLogAction m
logHtml HtmlLogAction (ReaderT (HtmlLogAction m) m)
-> HtmlLogAction (ReaderT (HtmlLogAction m) m)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
[ String
"Warning: HTML is currently generated for ALL files which can be"
, String
"reached from the given module, including library files."
]
let opts :: HtmlOptions
opts = HtmlFlags -> HtmlOptions
htmlOptsOfFlags HtmlFlags
flags
HtmlOptions -> ReaderT (HtmlLogAction m) m ()
forall (m :: * -> *). MonadIO m => HtmlOptions -> m ()
prepareCommonDestinationAssets HtmlOptions
opts
HtmlCompileEnv -> LogHtmlT m HtmlCompileEnv
forall a. a -> ReaderT (HtmlLogAction m) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (HtmlCompileEnv -> LogHtmlT m HtmlCompileEnv)
-> HtmlCompileEnv -> LogHtmlT m HtmlCompileEnv
forall a b. (a -> b) -> a -> b
$ HtmlOptions -> HtmlCompileEnv
HtmlCompileEnv HtmlOptions
opts
preModuleHtml
:: Applicative m
=> HtmlCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe FilePath
-> m (Recompile HtmlModuleEnv HtmlModule)
preModuleHtml :: forall (m :: * -> *).
Applicative m =>
HtmlCompileEnv
-> IsMain
-> TopLevelModuleName
-> Maybe String
-> m (Recompile HtmlModuleEnv HtmlModule)
preModuleHtml HtmlCompileEnv
cenv IsMain
_isMain TopLevelModuleName
modName Maybe String
_ifacePath = Recompile HtmlModuleEnv HtmlModule
-> m (Recompile HtmlModuleEnv HtmlModule)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Recompile HtmlModuleEnv HtmlModule
-> m (Recompile HtmlModuleEnv HtmlModule))
-> Recompile HtmlModuleEnv HtmlModule
-> m (Recompile HtmlModuleEnv HtmlModule)
forall a b. (a -> b) -> a -> b
$ HtmlModuleEnv -> Recompile HtmlModuleEnv HtmlModule
forall menv mod. menv -> Recompile menv mod
Recompile (HtmlCompileEnv -> TopLevelModuleName -> HtmlModuleEnv
HtmlModuleEnv HtmlCompileEnv
cenv TopLevelModuleName
modName)
compileDefHtml
:: Applicative m
=> HtmlCompileEnv
-> HtmlModuleEnv
-> IsMain
-> Definition
-> m HtmlDef
compileDefHtml :: forall (m :: * -> *).
Applicative m =>
HtmlCompileEnv
-> HtmlModuleEnv -> IsMain -> Definition -> m HtmlDef
compileDefHtml HtmlCompileEnv
_env HtmlModuleEnv
_menv IsMain
_isMain Definition
_def = HtmlDef -> m HtmlDef
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HtmlDef
HtmlDef
postModuleHtml
:: (MonadIO m, MonadDebug m, ReadTCState m)
=> HtmlCompileEnv
-> HtmlModuleEnv
-> IsMain
-> TopLevelModuleName
-> [HtmlDef]
-> m HtmlModule
postModuleHtml :: forall (m :: * -> *).
(MonadIO m, MonadDebug m, ReadTCState m) =>
HtmlCompileEnv
-> HtmlModuleEnv
-> IsMain
-> TopLevelModuleName
-> [HtmlDef]
-> m HtmlModule
postModuleHtml HtmlCompileEnv
_env HtmlModuleEnv
menv IsMain
_isMain TopLevelModuleName
_modName [HtmlDef]
_defs = do
let generatePage :: HtmlInputSourceFile -> ReaderT (HtmlLogAction m) m ()
generatePage = HtmlOptions
-> HtmlInputSourceFile -> ReaderT (HtmlLogAction m) m ()
forall (m :: * -> *).
(MonadIO m, MonadLogHtml m) =>
HtmlOptions -> HtmlInputSourceFile -> m ()
defaultPageGen (HtmlOptions
-> HtmlInputSourceFile -> ReaderT (HtmlLogAction m) m ())
-> (HtmlModuleEnv -> HtmlOptions)
-> HtmlModuleEnv
-> HtmlInputSourceFile
-> ReaderT (HtmlLogAction m) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HtmlCompileEnv -> HtmlOptions
htmlCompileEnvOpts (HtmlCompileEnv -> HtmlOptions)
-> (HtmlModuleEnv -> HtmlCompileEnv)
-> HtmlModuleEnv
-> HtmlOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HtmlModuleEnv -> HtmlCompileEnv
htmlModEnvCompileEnv (HtmlModuleEnv
-> HtmlInputSourceFile -> ReaderT (HtmlLogAction m) m ())
-> HtmlModuleEnv
-> HtmlInputSourceFile
-> ReaderT (HtmlLogAction m) m ()
forall a b. (a -> b) -> a -> b
$ HtmlModuleEnv
menv
HtmlInputSourceFile
htmlSrc <- TopLevelModuleName -> Interface -> HtmlInputSourceFile
srcFileOfInterface (HtmlModuleEnv -> TopLevelModuleName
htmlModEnvName HtmlModuleEnv
menv) (Interface -> HtmlInputSourceFile)
-> m Interface -> m HtmlInputSourceFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Interface
forall (m :: * -> *). ReadTCState m => m Interface
curIF
ReaderT (HtmlLogAction m) m () -> m ()
forall (m :: * -> *) a. MonadDebug m => LogHtmlT m a -> m a
runLogHtmlWithMonadDebug (ReaderT (HtmlLogAction m) m () -> m ())
-> ReaderT (HtmlLogAction m) m () -> m ()
forall a b. (a -> b) -> a -> b
$ HtmlInputSourceFile -> ReaderT (HtmlLogAction m) m ()
generatePage HtmlInputSourceFile
htmlSrc
HtmlModule -> m HtmlModule
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return HtmlModule
HtmlModule
postCompileHtml
:: Applicative m
=> HtmlCompileEnv
-> IsMain
-> Map TopLevelModuleName HtmlModule
-> m ()
postCompileHtml :: forall (m :: * -> *).
Applicative m =>
HtmlCompileEnv
-> IsMain -> Map TopLevelModuleName HtmlModule -> m ()
postCompileHtml HtmlCompileEnv
_cenv IsMain
_isMain Map TopLevelModuleName HtmlModule
_modulesByName = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()