From b9421b9a12b148d9279a881cce227affdb09ed08 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 27 Mar 2023 14:38:13 +0200 Subject: [PATCH] fix: Use Z(separator) instead of S(ymbol) category closes: #123 --- DocGen4/Output/DocString.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index a769148..ef75d76 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -57,7 +57,7 @@ partial def xmlGetHeadingId (el : Xml.Element) : String := unicodeToDrop (c : Char) : Bool := let cats := [ Unicode.GeneralCategory.P, -- punctuation - Unicode.GeneralCategory.S, -- separator + Unicode.GeneralCategory.Z, -- separator Unicode.GeneralCategory.C -- other ] cats.any (Unicode.isInGeneralCategory c) @@ -179,7 +179,7 @@ def autoLink (el : Element) : HtmlM Element := do return [Content.Character s] unicodeToSplit (c : Char) : Bool := let cats := [ - Unicode.GeneralCategory.S, -- separator + Unicode.GeneralCategory.Z, -- separator Unicode.GeneralCategory.C -- other ] cats.any (Unicode.isInGeneralCategory c)