diff --git a/Mdgen/Analyze.lean b/Mdgen/Analyze.lean index 611ea82..bd9f684 100644 --- 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 index d68d35d..3d7b074 100644 --- 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 index a2de5f8..98fe2bb 100644 --- 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 index 3ed453d..f6ed815 100644 --- 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! -/