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