Skip to content

Commit

Permalink
fix function name
Browse files Browse the repository at this point in the history
  • Loading branch information
Seasawher committed Feb 4, 2025
1 parent 1ed9fcd commit 74d2205
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 10 deletions.
16 changes: 8 additions & 8 deletions Mdgen/Analysis.lean → Mdgen/Analyze.lean
Original file line number Diff line number Diff line change
Expand Up @@ -33,15 +33,15 @@ def filterIgnored (lines : List String) : List String := Id.run do
return res.reverse

/-- Receive a list of codes and count the nesting of block and sectioning comments.
* The corresponding opening and closing brackets should have the same level.
* Also handles the exclusion of ignored targets.
The corresponding opening and closing brackets should have the same level.
-/
def analysis (lines : List String) : List RichLine := Id.run do
def analyze (lines : List String) : List RichLine := Id.run do
let lines := filterIgnored lines
let mut res : List RichLine := []
let mut level := 0
let mut doc := false
let mut blockCommentInDoc := false
for line in (filterIgnored lines) do
for line in lines do
if line.startsWith "/--" then
doc := true
if line.startsWith "/-" && ! line.startsWith "/--" then
Expand All @@ -58,13 +58,13 @@ def analysis (lines : List String) : List RichLine := Id.run do
blockCommentInDoc := false
return res.reverse

namespace Analysis
namespace Analyze

set_option linter.unusedVariables false in

/-- test for `analysis` function -/
/-- test for `analyze` function -/
def runTest (title := "") (input : List String) (expected : List (Nat × Bool)) : IO Unit := do
let output := analysis input |>.map (fun x => (x.level, x.close))
let output := analyze input |>.map (fun x => (x.level, x.close))
if output ≠ expected then
throw <| .userError s!"Test failed: \n{output}"

Expand Down Expand Up @@ -131,4 +131,4 @@ def runTest (title := "") (input : List String) (expected : List (Nat × Bool))
]
[(0, false)]

end Analysis
end Analyze
4 changes: 2 additions & 2 deletions Mdgen/ConvertToMd.lean
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import Mdgen.Analysis
import Mdgen.Analyze

/-- A chunk of grouped code for conversion to markdown. -/
structure Block where
Expand Down Expand Up @@ -89,7 +89,7 @@ def Block.postProcess (outputFilePath outputDir : FilePath) (b : Block) : Block

/-- convert lean contents to markdown contents. -/
def convertToMd (outputFilePath outputDir : Option FilePath := none) (lines : List String) : Md :=
let blocks := buildBlocks <| analysis lines
let blocks := buildBlocks <| analyze lines

let postProcessedBlocks :=
match outputFilePath, outputDir with
Expand Down

0 comments on commit 74d2205

Please sign in to comment.