scratches/doug
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

controlling the display of dotfiles
Some checks are pending
Lean Action CI / build (push) Waiting to run
Details

Browse source
This commit is contained in:
qwjyh 2024-10-22 18:02:57 +09:00
parent e2003d0898
commit de3fe6dd6d
1 changed files with 19 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
Doug/Basic.lean
View file

@ -2,6 +2,7 @@ def hello := "world"
structure Config where structure Config where
useASCII : Bool := false useASCII : Bool := false
printAll : Bool := false
currentPrefix : String := "" currentPrefix : String := ""
abbrev ConfigIO (α : Type) : Type := ReaderT Config IO α abbrev ConfigIO (α : Type) : Type := ReaderT Config IO α
@ -20,12 +21,16 @@ def currentConfig : ConfigIO Config :=
def usage : String := def usage : String :=
"Usage: doug [--ascii] "Usage: doug [--ascii]
Options: Options:
\t--ascii\tUse ASCII characters to display the directry structure" \t--ascii\tUse ASCII characters to display the directry structure
\t-a\tShow hidden entries"
def configFromArgs : List String → Option Config def configFromArgs (args : List String) : Option Config :=
| [] => some {} let parse_arg cfg arg :=
| ["--ascii"] => some {useASCII := true} match arg with
| "--ascii" => some {cfg with useASCII := true}
| "-a" => some {cfg with printAll := true}
| _ => none | _ => none
args.foldlM parse_arg {}
inductive Entry where inductive Entry where
| file : String → Entry | file : String → Entry
@ -65,8 +70,11 @@ def doList [Applicative f] : List α → (α → f Unit) → f Unit
partial def dirTree (path : System.FilePath) : ConfigIO Unit := do partial def dirTree (path : System.FilePath) : ConfigIO Unit := do
match ← toEntry path with match ← toEntry path with
| none => pure () | none => pure ()
| some (.file name) => showFileName name | some (.file name) =>
if ((← read).printAll) || !(name.startsWith ".") then
showFileName name
| some (.dir name) => | some (.dir name) =>
if ((← read).printAll) || !(name.startsWith ".") then
showDirName name showDirName name
let contents ← path.readDir let contents ← path.readDir
withReader (·.inDirectory) withReader (·.inDirectory)