From 755f06fb0d6e3ae4acbd7814ec75cac6ae83f104 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Sat, 11 Mar 2023 14:57:14 -0500 Subject: [PATCH] fix: correct character category testing --- DocGen4/Output/DocString.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index c58804d..0f1468e 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -55,13 +55,12 @@ partial def xmlGetHeadingId (el : Xml.Element) : String := |>.filter (!ยท.isEmpty) |> replacement.intercalate unicodeToDrop (c : Char) : Bool := - let generalCategory := Unicode.getGeneralCategory c let cats := [ Unicode.GeneralCategory.P, -- punctuation Unicode.GeneralCategory.S, -- separator Unicode.GeneralCategory.C -- other ] - cats.elem generalCategory + cats.any (Unicode.isInGeneralCategory c) /-- This function try to find the given name, both globally and in current module. @@ -179,12 +178,11 @@ def autoLink (el : Element) : HtmlM Element := do | none => return [Content.Character s] unicodeToSplit (c : Char) : Bool := - let generalCategory := Unicode.getGeneralCategory c let cats := [ Unicode.GeneralCategory.S, -- separator Unicode.GeneralCategory.C -- other ] - cats.elem generalCategory + cats.any (Unicode.isInGeneralCategory c) /-- Core function of modifying the cmark rendered docstring html. -/ partial def modifyElement (element : Element) : HtmlM Element :=