
   0 | module Katla.CLI
   1 | 
   2 | import public Collie
   3 | 
   4 | import Katla.Config
   5 | import Katla.LaTeX
   6 | import Katla.HTML
   7 | import Katla.Engine
   8 | 
   9 | %default covering
  10 | %hide Collie.Modifiers.infix.(::=)
  11 | 
  12 | export
  13 | failWithUsage : {nm : _} -> Command nm -> IO ()
  14 | failWithUsage cmd
  15 |   = do putStrLn cmd.usage
  16 |        exitFailure
  17 | 
  18 | export
  19 | inlineCmd : Command "inline"
  20 | inlineCmd = MkCommand
  21 |   { description = """
  22 |       Generate a macro that typesets an inline code snippet
  23 |       """
  24 |   , subcommands = []
  25 |   , modifiers = []
  26 |   , arguments = lotsOf filePath
  27 |   }
  28 | 
  29 | export
  30 | macroCmd : Command "macro"
  31 | macroCmd = MkCommand
  32 |   { description = """
  33 |       Generate a macro that typesets the code snippet
  34 |       """
  35 |   , subcommands = ["inline" ::= inlineCmd]
  36 |   , modifiers = []
  37 |   , arguments = lotsOf filePath
  38 |   }
  39 | 
  40 | export
  41 | markdownCmd : Command "markdown"
  42 | markdownCmd = MkCommand
  43 |   { description = "Markdown backend"
  44 |   , subcommands =
  45 |     [ "init"     ::= initHTMLCmd
  46 |     ]
  47 |   , modifiers   = ["--config" ::= option """
  48 |                     Preamble configuration file in Dhall format.
  49 |                     Use `init` to generate the defaults config file.
  50 |                     """ filePath
  51 |                   -- TODO: support for snippets
  52 |                   -- , "--snippet" ::= flag """
  53 |                   --   Generates a standalone LaTeX file when unset or just \
  54 |                   --   a code snippet when set.
  55 |                   --   Default: unset/false.
  56 |                   --   """
  57 |                   ]
  58 |   , arguments = lotsOf filePath
  59 |   }
  60 | 
  61 | export
  62 | literateCmd : Command "literate"
  63 | literateCmd = MkCommand
  64 |   { description = "Literate LaTeX backend"
  65 |   , subcommands =
  66 |     [ "init"     ::= initLatexCmd
  67 |     ]
  68 |   , modifiers   = ["--config" ::= option """
  69 |                     Preamble configuration file in Dhall format.
  70 |                     Use `init` to generate the defaults config file.
  71 |                     """ filePath
  72 |                   -- TODO: support for snippets
  73 |                   -- , "--snippet" ::= flag """
  74 |                   --   Generates a standalone LaTeX file when unset or just \
  75 |                   --   a code snippet when set.
  76 |                   --   Default: unset/false.
  77 |                   --   """
  78 |                   ]
  79 |   , arguments = lotsOf filePath
  80 |   }
  81 | 
  82 | export
  83 | htmlCmd : Command "html"
  84 | htmlCmd = MkCommand
  85 |   { description = """
  86 |     HTML backend
  87 |     Usage: html Katla.idr build/ttc/*/Katla.ttm > out.html
  88 |     """
  89 |   , subcommands =
  90 |     [ "init"     ::= initHTMLCmd
  91 |     ]
  92 |   , modifiers   = ["--config" ::= option """
  93 |                     Preamble configuration file in Dhall format.
  94 |                     Use `init` to generate the defaults config file.
  95 |                     """ filePath
  96 |                   -- TODO: support for snippets
  97 |                   -- , "--snippet" ::= flag """
  98 |                   --   Generates a standalone LaTeX file when unset or just \
  99 |                   --   a code snippet when set.
 100 |                   --   Default: unset/false.
 101 |                   --   """
 102 |                   ]
 103 |   , arguments = lotsOf filePath
 104 |   }
 105 | 
 106 | export
 107 | latexCmd : Command "latex"
 108 | latexCmd = MkCommand
 109 |   { description = "LaTeX backend"
 110 |   , subcommands =
 111 |     [ "preamble" ::= preambleCmd
 112 |     , "init"     ::= initLatexCmd
 113 |     , "macro"    ::= macroCmd
 114 |     ]
 115 |   , modifiers   = ["--config" ::= option """
 116 |                     Preamble configuration file in Dhall format.
 117 |                     Use `init` to generate the defaults config file.
 118 |                     """ filePath
 119 |                   , "--snippet" ::= flag """
 120 |                     Generates a standalone LaTeX file when unset or just \
 121 |                     a code snippet when set.
 122 |                     Default: unset/false.
 123 |                     """
 124 |                   ]
 125 |   , arguments = lotsOf filePath
 126 |   }
 127 | 
 128 | export
 129 | katlaCmd : Command "katla"
 130 | katlaCmd = MkCommand
 131 |   { description = """
 132 |       Katla v0.2.
 133 |       Code listing generator for Idris2
 134 |       """
 135 |   , subcommands =
 136 |     [ "--help"   ::= basic "Print this help text." none
 137 |     , "latex"    ::= latexCmd
 138 |     , "html"     ::= htmlCmd
 139 |     , "markdown" ::= markdownCmd
 140 |     , "literate" ::= literateCmd
 141 |     ]
 142 |   , modifiers = []
 143 |   , arguments = none
 144 |   }
 145 | 
 146 | rawSnippet : Bool -> Maybe Snippet
 147 | rawSnippet False = Nothing
 148 | rawSnippet True  = Just (Raw Nothing)
 149 | 
 150 | katlaLatexExec : CLI.latexCmd ~~> IO ()
 151 | katlaLatexExec =
 152 |   [ \parsed => case parsed.arguments of
 153 |        Just [src, md, output] =>
 154 |          katla LaTeX
 155 |                (rawSnippet $ parsed.modifiers.project "--snippet")
 156 |                (parsed.modifiers.project "--config")
 157 |                (Just src) (Just md) (Just output)
 158 |        Just [src, md]         =>
 159 |          katla LaTeX
 160 |                (rawSnippet $ parsed.modifiers.project "--snippet")
 161 |                (parsed.modifiers.project "--config")
 162 |                (Just src) (Just md) Nothing
 163 |        _ => failWithUsage latexCmd
 164 |   , "macro"   ::=
 165 |     [\parsed => case parsed.arguments of
 166 |       Just [name, src, md, output] =>
 167 |         katla LaTeX
 168 |               (Just $ Macro (name, False, Nothing))
 169 |               Nothing
 170 |               (Just src) (Just md) (Just output)
 171 |       Just [name, src, md, output, offset, before, after] =>
 172 |         katla LaTeX
 173 |               (Just $ Macro (name, False, Just $ RowRangeByOffset
 174 |                                     { offset = cast offset - 1
 175 |                                     , before = cast before
 176 |                                     , after  = cast after}))
 177 |               Nothing
 178 |               (Just src) (Just md) (Just output)
 179 |       Just [name, src, md, offset, before, after] =>
 180 |         katla LaTeX
 181 |               (Just $ Macro (name, False, Just $ RowRangeByOffset
 182 |                                     { offset = cast offset - 1
 183 |                                     , before = cast before
 184 |                                     , after  = cast after}))
 185 |               Nothing
 186 |               (Just src) (Just md) Nothing
 187 | 
 188 |       Just [name, src, md] =>
 189 |         katla LaTeX
 190 |               (Just $ Macro (name, False, Nothing))
 191 |               Nothing
 192 |               (Just src) (Just md) Nothing
 193 |       _ => failWithUsage latexCmd
 194 |     , "inline" ::= [\parsed => case parsed.arguments of
 195 |       Just [name, src, md, output, offset, line, startCol, endCol] =>
 196 |         katla LaTeX
 197 |               (Just $ Macro (name, True, Just (RangeByOffsetAndCols
 198 |                                     { offset = cast offset - 1
 199 |                                     , after  = cast line
 200 |                                     , startCol  = cast startCol - 1
 201 |                                     , endCol    = cast endCol
 202 |                                     })))
 203 |               Nothing
 204 |               (Just src) (Just md) (Just output)
 205 |       Just [name, src, md,         offset, line, startCol, endCol] => do
 206 |         katla LaTeX
 207 |               (Just $ Macro (name, True, Just (RangeByOffsetAndCols
 208 |                                     { offset = cast offset - 1
 209 |                                     , after  = cast line
 210 |                                     , startCol  = cast startCol - 1
 211 |                                     , endCol    = cast endCol
 212 |                                     })))
 213 |               Nothing
 214 |               (Just src) (Just md) Nothing
 215 |       _ => failWithUsage latexCmd
 216 |       ]
 217 |     ]
 218 |   , "preamble" ::= [preamble]
 219 |   , "init"     ::= [LaTeX.init]
 220 |   ]
 221 | 
 222 | katlaMarkdownExec : CLI.markdownCmd ~~> IO ()
 223 | katlaMarkdownExec =
 224 |   [ \parsed => case parsed.arguments of
 225 |        Just [src, md, output] =>
 226 |          katla Markdown
 227 |                Nothing -- (rawSnippet $ parsed.modifiers.project "--snippet")
 228 |                (parsed.modifiers.project "--config")
 229 |                (Just src) (Just md) (Just output)
 230 |        Just [src, md]         =>
 231 |          katla Markdown
 232 |                Nothing -- (rawSnippet $ parsed.modifiers.project "--snippet")
 233 |                (parsed.modifiers.project "--config")
 234 |                (Just src) (Just md) Nothing
 235 |        _ => failWithUsage markdownCmd
 236 |   , "init"     ::= [HTML.init]
 237 |   ]
 238 | 
 239 | katlaLiterateExec : CLI.literateCmd ~~> IO ()
 240 | katlaLiterateExec =
 241 |   [ \parsed => case parsed.arguments of
 242 |        Just [src, md, output] => do
 243 |          katla Literate
 244 |                Nothing -- (rawSnippet $ parsed.modifiers.project "--snippet")
 245 |                (parsed.modifiers.project "--config")
 246 |                (Just src) (Just md) (Just output)
 247 |        Just [src, md] => do
 248 |          katla Literate
 249 |                Nothing -- (rawSnippet $ parsed.modifiers.project "--snippet")
 250 |                (parsed.modifiers.project "--config")
 251 |                (Just src) (Just md) Nothing
 252 |        _ => failWithUsage literateCmd
 253 |   , "init"     ::= [LaTeX.init]
 254 |   ]
 255 | 
 256 | katlaHTMLExec : CLI.htmlCmd ~~> IO ()
 257 | katlaHTMLExec =
 258 |   [ \parsed => case parsed.arguments of
 259 |        Just [src, md, output] =>
 260 |          katla HTML
 261 |                Nothing -- (rawSnippet $ parsed.modifiers.project "--snippet")
 262 |                (parsed.modifiers.project "--config")
 263 |                (Just src) (Just md) (Just output)
 264 |        Just [src, md]         =>
 265 |          katla HTML
 266 |                Nothing -- (rawSnippet $ parsed.modifiers.project "--snippet")
 267 |                (parsed.modifiers.project "--config")
 268 |                (Just src) (Just md) Nothing
 269 |        _ => failWithUsage htmlCmd
 270 |   , "init"     ::= [HTML.init]
 271 |   ]
 272 | 
 273 | export
 274 | katlaExec : CLI.katlaCmd ~~> IO ()
 275 | katlaExec =
 276 |   [ const (failWithUsage katlaCmd)
 277 |   , "--help"   ::= [ const (putStrLn katlaCmd.usage) ]
 278 |   , "latex"    ::= katlaLatexExec
 279 |   , "html"     ::= katlaHTMLExec
 280 |   , "markdown" ::= katlaMarkdownExec
 281 |   , "literate" ::= katlaLiterateExec
 282 |   ]
 283 |