0 | ||| Functions for generating
  1 | module Katla.LaTeX
  2 |
  3 | import Core.Metadata
  4 | import System.File
  5 |
  6 | import Collie
  7 | import Katla.Config
  8 |
  9 | %hide Collie.Modifiers.infix.(::=)
 10 |
 11 | export
 12 | escapeLatex : Char -> List Char
 13 | escapeLatex '-' = fastUnpack "\\KatlaDash{}"
 14 | escapeLatex '&' = fastUnpack "\\&"
 15 | escapeLatex '%' = fastUnpack "\\%"
 16 | escapeLatex '\\' = fastUnpack "\\textbackslash{}"
 17 | escapeLatex '#'  = fastUnpack "\\#"
 18 | escapeLatex '{'  = fastUnpack "\\{"
 19 | escapeLatex '}'  = fastUnpack "\\}"
 20 | escapeLatex '$'  = fastUnpack "\\$"
 21 | escapeLatex ' '  = fastUnpack "\\KatlaSpace{}"
 22 | escapeLatex '_'  = fastUnpack "\\KatlaUnderscore{}"
 23 | escapeLatex '~'  = fastUnpack "\\KatlaTilde{}"
 24 | escapeLatex x    = [x]
 25 |
 26 | export
 27 | annotate : Maybe Decoration -> String -> String
 28 | annotate Nothing    s = s
 29 | annotate (Just dec) s = apply (convert dec) s
 30 |   where
 31 |
 32 |     apply : String -> String -> String
 33 |     apply f a = "\\\{f}{\{a}}"
 34 |
 35 | export
 36 | laTeXHeader : Config -> String
 37 | laTeXHeader cfg =  """
 38 | \\usepackage{fancyvrb}
 39 | \\usepackage[x11names]{xcolor}
 40 | \\newcommand{\\Katla}                [2][]{\\VerbatimInput[commandchars=\\\\\\{\\}#1]{#2}}
 41 | \\newcommand{\\KatlaNewline}            {}
 42 | \\newcommand{\\KatlaSpace}              {\{cfg.space}}
 43 | \\newcommand{\\KatlaDash}               {\\string-}
 44 | \\newcommand{\\KatlaUnderscore}         {\\string_}
 45 | \\newcommand{\\KatlaTilde}              {\\string~}
 46 | \\newcommand{\\IdrisHlightFont}         {\{cfg.font}}
 47 | \\newcommand{\\IdrisHlightStyleData}    {\{cfg.datacons .style}}
 48 | \\newcommand{\\IdrisHlightStyleType}    {\{cfg.typecons .style}}
 49 | \\newcommand{\\IdrisHlightStyleBound}   {\{cfg.bound    .style}}
 50 | \\newcommand{\\IdrisHlightStyleFunction}{\{cfg.function .style}}
 51 | \\newcommand{\\IdrisHlightStyleKeyword} {\{cfg.keyword  .style}}
 52 | \\newcommand{\\IdrisHlightStyleImplicit}{\{cfg.bound    .style}}
 53 | \\newcommand{\\IdrisHlightStyleComment} {\{cfg.comment  .style}}
 54 | \\newcommand{\\IdrisHlightStyleHole}    {\{cfg.hole     .style}}
 55 | \\newcommand{\\IdrisHlightStyleNamespace}{\{cfg.namespce.style}}
 56 | \\newcommand{\\IdrisHlightStylePostulate}{\{cfg.postulte.style}}
 57 | \\newcommand{\\IdrisHlightStyleModule}   {\{cfg.aModule .style}}
 58 |
 59 | \\newcommand{\\IdrisHlightColourData}    {\{cfg.datacons .colour}}
 60 | \\newcommand{\\IdrisHlightColourType}    {\{cfg.typecons .colour}}
 61 | \\newcommand{\\IdrisHlightColourBound}   {\{cfg.bound    .colour}}
 62 | \\newcommand{\\IdrisHlightColourFunction}{\{cfg.function .colour}}
 63 | \\newcommand{\\IdrisHlightColourKeyword} {\{cfg.keyword  .colour}}
 64 | \\newcommand{\\IdrisHlightColourImplicit}{\{cfg.bound    .colour}}
 65 | \\newcommand{\\IdrisHlightColourComment} {\{cfg.comment  .colour}}
 66 | \\newcommand{\\IdrisHlightColourHole}    {\{cfg.hole     .colour}}
 67 | \\newcommand{\\IdrisHlightColourNamespace}{\{cfg.namespce.colour}}
 68 | \\newcommand{\\IdrisHlightColourPostulate}{\{cfg.postulte.colour}}
 69 | \\newcommand{\\IdrisHlightColourModule}   {\{cfg.aModule .colour}}
 70 |
 71 | \\newcommand{\\IdrisHole}[1]{{%
 72 |     \\colorbox{\\IdrisHlightColourHole}{%
 73 |       \\IdrisHlightStyleHole\\IdrisHlightFont%
 74 |       #1}}}
 75 |
 76 | \\newcommand{\\RawIdrisHighlight}[3]{{\\textcolor{#1}{\\IdrisHlightFont#2{#3}}}}
 77 |
 78 | \\newcommand{\\IdrisData}[1]{\\RawIdrisHighlight{\\IdrisHlightColourData}{\\IdrisHlightStyleData}{#1}}
 79 | \\newcommand{\\IdrisType}[1]{\\RawIdrisHighlight{\\IdrisHlightColourType}{\\IdrisHlightStyleType}{#1}}
 80 | \\newcommand{\\IdrisBound}[1]{\\RawIdrisHighlight{\\IdrisHlightColourBound}{\\IdrisHlightStyleBound}{#1}}
 81 | \\newcommand{\\IdrisFunction}[1]{\\RawIdrisHighlight{\\IdrisHlightColourFunction}{\\IdrisHlightStyleFunction}{#1}}
 82 | \\newcommand{\\IdrisKeyword}[1]{\\RawIdrisHighlight{\\IdrisHlightColourKeyword}{\\IdrisHlightStyleKeyword}{#1}}
 83 | \\newcommand{\\IdrisImplicit}[1]{\\RawIdrisHighlight{\\IdrisHlightColourImplicit}{\\IdrisHlightStyleImplicit}{#1}}
 84 | \\newcommand{\\IdrisComment}[1]{\\RawIdrisHighlight{\\IdrisHlightColourComment}{\\IdrisHlightStyleComment}{#1}}
 85 | \\newcommand{\\IdrisNamespace}[1]{\\RawIdrisHighlight{\\IdrisHlightColourNamespace}{\\IdrisHlightStyleNamespace}{#1}}
 86 | \\newcommand{\\IdrisPostulate}[1]{\\RawIdrisHighlight{\\IdrisHlightColourPostulate}{\\IdrisHlightStylePostulate}{#1}}
 87 | \\newcommand{\\IdrisModule}[1]{\\RawIdrisHighlight{\\IdrisHlightColourModule}{\\IdrisHlightStyleModule}{#1}}
 88 |
 89 | \\DefineVerbatimEnvironment%
 90 | {code}{Verbatim}{commandchars=\\\\\\{\\}}
 91 |
 92 | % Bugfix in fancyvrb to allow inline saved listings
 93 | \\makeatletter
 94 | \\let\\FV@ProcessLine\\relax
 95 | \\makeatother
 96 |
 97 | """
 98 |
 99 |
100 | export
101 | standalonePre : Config -> String
102 | standalonePre config = """
103 |   \\documentclass{article}
104 |
105 |   \\usepackage{inconsolata}
106 |
107 |   \{laTeXHeader config}
108 |
109 |   \\begin{document}
110 |   \\begin{Verbatim}[commandchars=\\\\\\{\\}]
111 |   """
112 |
113 | export
114 | standalonePost : String
115 | standalonePost = """
116 |   \\end{Verbatim}
117 |   \\end{document}
118 |   """
119 |
120 | export
121 | makeMacroPre : String -> String
122 | makeMacroPre name = """
123 |   \\newcommand\\\{name}[1][]{\\UseVerbatim[#1]{\{name}}}
124 |   \\begin{SaveVerbatim}[commandchars=\\\\\\{\\}]{\{name}}
125 |   """
126 |
127 | export
128 | makeMacroPost : String
129 | makeMacroPost = """
130 |   \\end{SaveVerbatim}
131 |   """
132 |
133 | export
134 | makeInlineMacroPre : String -> String
135 | makeInlineMacroPre name = """
136 |   \\newcommand\\\{name}[1][]{\\UseVerb[#1]{\{name}}}
137 |   \\begin{SaveVerbatim}[commandchars=\\\\\\{\\}]{\{name}}
138 |   """
139 |
140 | export
141 | makeInlineMacroPost : String
142 | makeInlineMacroPost = """
143 |   \\end{SaveVerbatim}
144 |   """
145 |
146 | export
147 | mkDriver : Config -> Driver
148 | mkDriver config = MkDriver
149 |   (\_, _ => "", "\\KatlaNewline{}")
150 |   escapeLatex
151 |   annotate
152 |   (standalonePre config, standalonePost)
153 |   (makeInlineMacroPre, makeInlineMacroPost)
154 |   (makeMacroPre, makeMacroPost)
155 |
156 | public export
157 | preambleCmd : Command "preamble"
158 | preambleCmd = MkCommand
159 |   { description = "Generate LaTeX preamble"
160 |   , subcommands = []
161 |   , modifiers =
162 |     [ "--config" ::= option """
163 |         Preamble configuration file in Dhall format.
164 |         Use `init` to generate the defaults config file.
165 |         """
166 |         filePath
167 |     ]
168 |   , arguments = filePath
169 |   }
170 |
171 | public export
172 | initLatexCmd : Command "init"
173 | initLatexCmd = MkCommand
174 |   { description = "Generate preamble configuration file"
175 |   , subcommands = []
176 |   , modifiers = []
177 |   , arguments = filePath
178 |   }
179 |
180 |
181 | preambleExec : (moutput : Maybe String) -> (configFile : Maybe String) -> IO ()
182 | preambleExec moutput configFile = do
183 |   Right file <- maybe (pure $ Right stdout) (flip openFile WriteTruncate) moutput
184 |   | Left err => putStrLn """
185 |               Error while opening preamble file \{maybe "stdout" id moutput}:
186 |               \{show err}
187 |               """
188 |   config <- getConfiguration LaTeX configFile
189 |   Right () <- fPutStr file $ laTeXHeader config
190 |   | Left err => putStrLn """
191 |       Error while writing preamble file \{fromMaybe "stdout" moutput}:
192 |       \{show err}
193 |       """
194 |   closeFile file
195 |
196 | export
197 | preamble : (ParsedCommand _ LaTeX.preambleCmd) -> IO ()
198 | preamble parsed = preambleExec parsed.arguments (parsed.modifiers.project "--config")
199 |
200 | export
201 | init : (ParsedCommand _ LaTeX.initLatexCmd) -> IO ()
202 | init parsed = initExec LaTeX parsed.arguments
203 |