fix indent breaking issue

Seasawher · Feb 4, 2025 · acdf321 · acdf321
1 parent 194c47f
commit acdf321
Show file tree

Hide file tree

Showing 4 changed files with 36 additions and 2 deletions.
diff --git a/Mdgen/Analyze.lean b/Mdgen/Analyze.lean
@@ -37,7 +37,7 @@ private def preprocess (lines : Array String) : Array Nat × Array String := Id.
   let token := "/-⋆-//--"
   let filtered : Array (Option Nat × String) :=
     lines.mapIdx (fun idx line =>
-      if line.startsWith token then
+      if line.trimLeft.startsWith token then
         (some idx, line.replace token "/--")
       else
         (none, line)
@@ -49,7 +49,7 @@ private def preprocess (lines : Array String) : Array Nat × Array String := Id.
 /-- postprocess for converting doc comment to block comment -/
 private def postprocess (indexes : Array Nat) (i : Nat) (line : String) : String :=
   if indexes.contains i then
-    "/-" ++ line.drop "/--".length
+    line.replace "/--" "/-"
   else
     line
 

diff --git a/Mdgen/ConvertToMd.lean b/Mdgen/ConvertToMd.lean
@@ -234,6 +234,23 @@ def runTest (input : List String) (expected : List String) (title := "") : IO Un
     "```"
   ]
 
+#eval runTest
+  (title := "convert doc comment syntax - indent")
+  [
+    "namespace Foo",
+    "  /-⋆-//-- doc comment -/",
+    "  def zero := 0",
+    "end Foo",
+  ]
+  [
+    "```lean",
+    "namespace Foo",
+    "  /- doc comment -/",
+    "  def zero := 0",
+    "end Foo",
+    "```"
+  ]
+
 #eval runTest
   (title := "multiple leading block comments in doc comment")
   [

diff --git a/Test/Exp/First.md b/Test/Exp/First.md
@@ -52,6 +52,14 @@ inductive MyNat where
 -- Here is a sample of converting doc comment to block comment
 /- info: MyNat.zero : MyNat -/
 #check MyNat.zero
+
+namespace MyNat
+  /- ## indent block -/
+
+  /- info: zero.succ : MyNat -/
+  #check MyNat.succ MyNat.zero
+
+end MyNat
 ```
 
 ## nested comment

diff --git a/Test/Src/First.lean b/Test/Src/First.lean
@@ -64,6 +64,15 @@ inductive MyNat where
 #guard_msgs in --#
 #check MyNat.zero
 
+namespace MyNat
+  /- ## indent block -/
+
+  /-⋆-//-- info: zero.succ : MyNat -/
+  #guard_msgs in --#
+  #check MyNat.succ MyNat.zero
+
+end MyNat
+
 /- ## nested comment
 Here is a sample of nested block comment:
 /- Hi. I am a nested comment! -/