diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index e2ae134..8fab52a 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -254,11 +254,12 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do | .sort _ => match t with | .text t => - let mut sortPrefix :: rest := t.splitOn " " | unreachable! + let sortPrefix :: rest := t.splitOn " " | unreachable! let sortLink := {sortPrefix} - if rest != [] then - rest := " " :: rest - return #[sortLink, Html.text <| String.join rest] + let mut restStr := String.intercalate " " rest + if restStr.length != 0 then + restStr := " " ++ restStr + return #[sortLink, Html.text restStr] | _ => return #[[← infoFormatToHtml t]] | _ =>