18
21
import qualified Data.Map as Map
19
22
import qualified Data.List as List
20
import qualified Agda.Utils.IO as UTF8
26
import Agda.Interaction.FindFile
24
27
import Agda.Interaction.Highlighting.Generate
25
28
import Agda.Interaction.Highlighting.Precise
26
29
import Agda.Interaction.Highlighting.Range
27
import qualified Agda.Interaction.Imports as Imp
28
30
import Agda.TypeChecking.Monad (TCM)
29
31
import qualified Agda.TypeChecking.Monad as TCM
30
32
import qualified Agda.Syntax.Abstract as A
33
import qualified Agda.Syntax.Concrete as C
31
34
import Agda.Syntax.Common
32
35
import qualified Agda.Syntax.Scope.Monad as Scope
33
36
import Agda.Syntax.Translation.ConcreteToAbstract
34
37
import Agda.Interaction.Options
38
import Agda.Utils.FileName (filePath)
39
import qualified Agda.Utils.IO.UTF8 as UTF8
40
import Agda.Utils.Pretty
42
import Agda.Utils.Impossible
43
#include "../../undefined.h"
36
45
-- | The name of the default CSS file.
58
67
cssFile <- getDataFileName defaultCSSFile
59
68
copyFile cssFile (dir </> defaultCSSFile)
61
TCM.reportSLn "html" 1 $
62
"\nWarning: HTML is currently generated for ALL files which can be\n\
63
\reached from the given module, including library files.\n"
70
TCM.reportSLn "html" 1 $ unlines
72
, "Warning: HTML is currently generated for ALL files which can be"
73
, "reached from the given module, including library files."
65
76
-- Pull highlighting info from the state and generate all the
67
78
mapM_ (\(m, h) -> generatePage dir m h) =<<
68
map (id *** TCM.iHighlighting) . Map.toList <$>
79
map (id *** TCM.iHighlighting . TCM.miInterface) .
80
Map.toList <$> TCM.getVisitedModules
71
82
-- | Converts module names to the corresponding HTML file names.
73
modToFile :: [String] -> FilePath
74
modToFile m = List.intercalate "." m <.> "html"
84
modToFile :: C.TopLevelModuleName -> FilePath
85
modToFile m = render (pretty m) <.> "html"
76
87
-- | Generates an HTML file with a highlighted, hyperlinked version of
77
88
-- the given module.
80
:: FilePath -- ^ Directory in which to create files.
81
-> A.ModuleName -- ^ Module to be highlighted.
82
-> HighlightingInfo -- ^ Syntax highlighting info for the module.
91
:: FilePath -- ^ Directory in which to create files.
92
-> C.TopLevelModuleName -- ^ Module to be highlighted.
93
-> HighlightingInfo -- ^ Syntax highlighting info for the module.
84
95
generatePage dir mod highlighting = do
85
contents <- liftIO $ UTF8.readTextFile (source highlighting)
86
css <- maybe defaultCSSFile id . optCSSFile <$>
87
TCM.commandLineOptions
88
let html = page css mod contents (info highlighting)
89
TCM.reportSLn "html" 1 $ "Generating HTML for " ++ show mod ++
90
" (" ++ target ++ ")."
91
liftIO $ UTF8.writeFile target (renderHtml html)
92
where target = dir </> modToFile (map show $ A.mnameToList mod)
96
mf <- Map.lookup mod . TCM.stModuleToSource <$> get
98
Nothing -> __IMPOSSIBLE__
100
contents <- liftIO $ UTF8.readTextFile $ filePath f
101
css <- maybe defaultCSSFile id . optCSSFile <$>
102
TCM.commandLineOptions
103
let html = page css mod contents highlighting
104
TCM.reportSLn "html" 1 $ "Generating HTML for " ++
105
render (pretty mod) ++
106
" (" ++ target ++ ")."
107
liftIO $ UTF8.writeFile target (renderHtml html)
108
where target = dir </> modToFile mod
94
110
-- | Constructs the web page, including headers.
96
page :: FilePath -- ^ URL to the CSS file.
97
-> A.ModuleName -- ^ Module to be highlighted.
98
-> String -- ^ The contents of the module.
99
-> CompressedFile -- ^ Highlighting information.
112
page :: FilePath -- ^ URL to the CSS file.
113
-> C.TopLevelModuleName -- ^ Module to be highlighted.
114
-> String -- ^ The contents of the module.
115
-> CompressedFile -- ^ Highlighting information.
101
117
page css modName contents info =
102
header (thetitle << show modName
118
header (thetitle << render (pretty modName)
104
120
meta ! [ httpequiv "Content-Type"
105
121
, content "text/html; charset=UTF-8"
added
removed
src/full/Agda/Interaction/Highlighting/HTML.hs
