From 74fcb1e5598aecb3f473ae0d2ece8bd79be89840 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Thu, 2 Jan 2025 20:56:32 +0900
Subject: [PATCH] count characters in markdown files Fixes #61

---
 Mdgen/Cli.lean | 13 ++++++++++++-
 lakefile.lean  |  2 +-
 2 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/Mdgen/Cli.lean b/Mdgen/Cli.lean
index 61dc0e7..a0ebb58 100644
--- a/Mdgen/Cli.lean
+++ b/Mdgen/Cli.lean
@@ -11,6 +11,14 @@ def runMdgenCmd (p : Parsed) : IO UInt32 := do
 
   let paths ← getLeanFilePaths inputDir
 
+  if p.hasFlag "count" then
+    let mut globalCount := 0
+    for path in paths do
+      let content ← IO.FS.lines path
+      let count := content.foldl (fun acc str => acc + str.length) 0
+      globalCount := globalCount + count
+    IO.println s!"The input Lean files contain a total of {globalCount} characters."
+
   for path in paths do
     let content ← IO.FS.lines path
 
@@ -25,9 +33,12 @@ def runMdgenCmd (p : Parsed) : IO UInt32 := do
 
 /-- API definition of `mdgen` command -/
 def mkMdgenCmd : Cmd := `[Cli|
-  mdgen VIA runMdgenCmd; ["1.5.0"]
+  mdgen VIA runMdgenCmd; ["1.6.0"]
   "mdgen is a tool to generate .md files from .lean files."
 
+  FLAGS:
+    c, count; "Counts the total number of characters in the input files. However, please be aware that the output may not be entirely accurate."
+
   ARGS:
     input_dir : String; "The directory containing the input Lean files."
     output_dir : String; "The directory to write the markdown files."
diff --git a/lakefile.lean b/lakefile.lean
index f89f2b4..634baf4 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -2,7 +2,7 @@ import Lake
 open Lake DSL
 
 package «mdgen» where
-  version := v!"1.5.0"
+  version := v!"1.6.0"
   keywords := #["cli", "markdown"]
   description := "Tool to generate markdown files from lean files."