0 | module Options

  2 | import Data.FilePath

  3 | import Data.List

  4 | import Data.List1

  5 | import Data.Nat

  6 | import Data.String

  7 | import Derive.Prelude

  8 | import Derive.Pretty

 10 | import System.GetOpts

 12 | %default total

 13 | %language ElabReflection

 19 | export %inline

 20 | Pretty Body where

 21 |   prettyPrec _ = line . interpolate

 23 | export %inline

 24 | Pretty FilePath where

 25 |   prettyPrec _ = line . interpolate

 28 | public export

 29 | record Config where

 30 |   constructor MkConfig

 32 |   ||| If True, prints only the program synopsis.

 33 |   printHelp     : Bool

 35 |   ||| Verbosity level. At the moment, 0 means total silence (errors are

 37 |   verbosity     : Nat

 39 |   ||| True, if files should only be checked for issues

 41 |   checkOnly     : Bool

 43 |   ||| True, if all non-hidden files should be checked when

 45 |   includeAll    : Bool

 47 |   ||| True, if hidden files should be checked when

 49 |   includeHidden : Bool

 51 |   ||| List of file extensions to be checked when traversing

 54 |   extensions    : List Body

 56 |   ||| List of files and directories to be checked.

 57 |   files         : List FilePath

 59 | %runElab derive "Config" [Show,Eq,Pretty]

 61 | init : List String -> Config

 62 | init fs =

 63 |   MkConfig

 64 |     { printHelp     = False

 65 |     , verbosity     = 2

 66 |     , checkOnly     = True

 67 |     , includeAll    = False

 68 |     , includeHidden = False

 69 |     , files         = case fs of [] => ["."]; _ => map fromString fs

 70 |     , extensions    = ["idr"]

 71 |     }

 76 | includeDir : FilePath -> Config -> Bool

 77 | includeDir p c = not (isHidden p) || c.includeHidden

 82 | includeFile : FilePath -> Config -> Bool

 83 | includeFile p c =

 84 |   let ext := extension p

 85 |    in c.includeAll || any ((ext ==) . Just) c.extensions

 91 | help : Config -> Config

 92 | help = {printHelp := True}

 94 | adjVerbosity : (Nat -> Nat) -> Config -> Config

 95 | adjVerbosity f = {verbosity $= f}

 97 | doFix : Bool -> Config -> Config

 98 | doFix b = {checkOnly := not b}

100 | setExts : String -> Config -> Config

101 | setExts s = {extensions := mapMaybe parse $ forget (split (',' ==) s)}

103 | setAll : Config -> Config

104 | setAll = {includeAll := True}

106 | setHidden : Config -> Config

107 | setHidden = {includeHidden := True}

109 | descs : List $ OptDescr (Config -> Config)

110 | descs =

111 |   [ MkOpt ['h'] ["help"]      (NoArg help)

112 |      "prints this help text\n "

113 |   , MkOpt ['v'] ["verbose"]   (NoArg $ adjVerbosity S)

114 |       "increase verbosity (default verbosity is 2)\n "

115 |   , MkOpt ['q'] ["quiet"]     (NoArg $ adjVerbosity pred)

116 |       "decrease verbosity (default verbosity is 2)\n "

117 |   , MkOpt ['c'] ["check"]     (NoArg $ doFix False)

118 |       "check and list files with issues (default)\n "

119 |   , MkOpt ['f'] ["fix"]       (NoArg $ doFix True)

120 |       "check and fix files with issues\n "

121 |   , MkOpt ['e'] ["ext"]       (ReqArg setExts "<exts>") $

122 |       unlines

123 |         [ "comma separated list of extensions of files"

124 |         , "to be included when traversing directories"

125 |         , "(default is \"idr\")."

126 |         , "Note: Files whose name starts with a dot will be"

127 |         , "ignored unless '--includeHidden' is set."

128 |         , ""

129 |         ]

130 |   , MkOpt ['a'] ["all"]       (NoArg setAll)

131 |       "include all non-hidden files when traversing directories\n "

132 |   , MkOpt []    ["includeHidden"] (NoArg setHidden) $

133 |       unlines

134 |         [ "include hidden files (name starts with a dot)"

135 |         , "when traversing directories"

136 |         , ""

137 |         ]

138 |   ]

141 | applyArgs : List String -> Either (List String) Config

142 | applyArgs args =

143 |   case getOpt RequireOrder descs args of

144 |     MkResult os n  [] [] => Right $ foldl (flip apply) (init n) os

145 |     MkResult _ _ u e       => Left $ map unknown u ++ e

147 |   where

148 |     unknown : String -> String

149 |     unknown = ("Unknown option: " ++)

155 | version : String

156 | version = "1.1.0"

158 | progName : String

159 | progName = "fix_whitespace"

161 | usage : String

162 | usage = "Usage: " ++ progName ++ " [options] [FILES]\n\nOptions:\n"

164 | synopsis : String

165 | synopsis =

166 |   unlines

167 |     [ progName ++ " version " ++ version

168 |     , ""

169 |     , "  Removes trailing whitespace characters from the specified"

170 |     , "  text files making sure every text file ends with exactly one"

171 |     , "  newline character. Windows style line breaks are replaced"

172 |     , "  by Unix newline characters."

173 |     , ""

174 |     , "  If the passed file list contains directories, " ++ progName

175 |     , "  will recursively adjust all files with the given extensions"

176 |     , "  (see option --ext) in those directories. If no files are"

177 |     , "  specified, the current directory will be traversed instead."

178 |     , ""

179 |     , usage

180 |     ]

183 | info : String

184 | info = usageInfo synopsis descs

187 | shortInfo : String

188 | shortInfo = usageInfo usage descs