[ agda#3366 ] Added initial support, will document later

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

src/full/Agda/Interaction/Highlighting/HTML.hs

@@ -130,10 +130,10 @@ generateHTMLWithPageGen generatePage = do
 
 -- | Converts module names to the corresponding HTML file names.
 
-modToFile :: C.TopLevelModuleName -> FilePath
-modToFile m =
+modToFile :: C.TopLevelModuleName -> String -> FilePath
+modToFile m ext =
   Network.URI.Encode.encode $
-    render (pretty m) <.> "html"
+    render (pretty m) <.> ext
 
 -- | Generates a highlighted, hyperlinked version of the given module.
 
@@ -148,12 +148,13 @@ generatePage renderPage dir mod = do
   f   <- fromMaybe __IMPOSSIBLE__ . Map.lookup mod <$> useTC TCM.stModuleToSource
   css <- fromMaybe defaultCSSFile . optCSSFile <$> TCM.commandLineOptions
   pc  <- optHTMLOnlyCode <$> TCM.commandLineOptions
+  ext <- optHTMLOutputExt <$> TCM.commandLineOptions
   let html = renderPage css pc $ filePath f
   TCM.reportSLn "html" 1 $ "Generating HTML for " ++
                            render (pretty mod) ++
                            " (" ++ target ++ ")."
   liftIO $ UTF8.writeTextToFile target html
-  where target = dir </> modToFile mod
+  where target = dir </> modToFile mod ext
 
 
 -- | Attach multiple Attributes
@@ -297,4 +298,4 @@ code asIs = mconcat . if asIs
         (++ "#" ++
          Network.URI.Encode.encode (show pos))
          -- Network.URI.Encode.encode (fromMaybe (show pos) aName)) -- Named links disabled
-        (Network.URI.Encode.encode $ modToFile m)
+        (Network.URI.Encode.encode $ modToFile m "html")

src/full/Agda/Interaction/Options.hs

@@ -33,6 +33,7 @@ import Control.Monad.Trans
 
 import Data.IORef
 import Data.Either
+import Data.Function
 import Data.Maybe
 import Data.List                ( isSuffixOf , intercalate )
 import Data.Set                 ( Set )
@@ -110,6 +111,7 @@ data CommandLineOptions = Options
   , optGenerateLaTeX    :: Bool
   , optGenerateHTML     :: Bool
   , optHTMLOnlyCode     :: Bool
+  , optHTMLOutputExt    :: String
   , optDependencyGraph  :: Maybe FilePath
   , optLaTeXDir         :: FilePath
   , optHTMLDir          :: FilePath
@@ -214,6 +216,7 @@ defaultOptions = Options
   , optGenerateLaTeX    = False
   , optGenerateHTML     = False
   , optHTMLOnlyCode     = False
+  , optHTMLOutputExt    = "html"
   , optDependencyGraph  = Nothing
   , optLaTeXDir         = defaultLaTeXDir
   , optHTMLDir          = defaultHTMLDir
@@ -296,13 +299,15 @@ type Flag opts = opts -> OptM opts
 
 checkOpts :: Flag CommandLineOptions
 checkOpts opts
+  | htmlRelated = throwError htmlRelatedMessage
   | not (matches [optGHCiInteraction, optJSONInteraction, isJust . optInputFile] <= 1) =
       throwError "Choose at most one: input file, --interactive, or --interaction-json.\n"
   | or [ p opts && matches ps > 1 | (p, ps) <- exclusive ] =
       throwError exclusiveMessage
   | otherwise = return opts
   where
   matches = length . filter ($ opts)
+  optionChanged opt = ((/=) `on` opt) opts defaultOptions
 
   atMostOne =
     [ optGenerateHTML
@@ -336,6 +341,18 @@ checkOpts opts
     , "--safe or --vim."
     ]
 
+  htmlRelated = optGenerateHTML opts &&
+    (  optionChanged optHTMLDir
+    || optionChanged optHTMLOnlyCode
+    || optionChanged optHTMLOutputExt
+    || optionChanged optCSSFile
+    )
+
+  htmlRelatedMessage = unlines $
+    [ "The options --html-highlight, --html-output-extention, --css-dir"
+    , "and --html-dir can only be used along with --html flag."
+    ]
+
 -- | Check for unsafe pramas. Gives a list of used unsafe flags.
 
 unsafePragmaOptions :: PragmaOptions -> [String]
@@ -581,6 +598,10 @@ htmlHighlightFlag "all"  o = return $ o { optHTMLOnlyCode = False }
 htmlHighlightFlag opt    o = throwError $ "Invalid option <" ++ opt
   ++ ">, expected <all> or <code>"
 
+-- TODO maybe validate file extension here?
+htmlOutputExtFlag :: String -> Flag CommandLineOptions
+htmlOutputExtFlag ext o = return $ o { optHTMLOutputExt = ext }
+
 dependencyGraphFlag :: FilePath -> Flag CommandLineOptions
 dependencyGraphFlag f o = return $ o { optDependencyGraph = Just f }
 
@@ -670,6 +691,8 @@ standardOptions =
                     "the CSS file used by the HTML files (can be relative)"
     , Option []     ["html-highlight"] (ReqArg htmlHighlightFlag "[code,all]")
                     "whether to highlight only the code parts (code) or the file as a whole (all)"
+    , Option []     ["html-output-extension"] (ReqArg htmlOutputExtFlag "EXT")
+                    "extension of the outputed html files (default: html)"
     , Option []     ["dependency-graph"] (ReqArg dependencyGraphFlag "FILE")
                     "generate a Dot file with a module dependency graph"
     , Option []     ["ignore-interfaces"] (NoArg ignoreInterfacesFlag)