fix: correctly split whitespace

leanprover · Dec 17, 2024 · 4cf1ae5 · 4cf1ae5
1 parent e473211
commit 4cf1ae5
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
@@ -256,10 +256,12 @@ only `+` should be linked, taking care of this is what this function is
 responsible for.
 -/
 def splitWhitespaces (s : String) : (String × String × String) := Id.run do
-  let front := "".pushn ' ' <| s.offsetOfPos (s.find (!Char.isWhitespace ·))
+  let mut length := s.length
   let mut s := s.trimLeft
-  let back := "".pushn ' ' (s.length - s.offsetOfPos (s.find Char.isWhitespace))
+  let front := "".pushn ' ' (length - s.length)
+  length := s.length
   s := s.trimRight
+  let back := "".pushn ' ' (length - s.length)
   (front, s, back)
 
 /--