diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 758b317..c58804d 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -1,9 +1,9 @@ import CMark import DocGen4.Output.Template import Lean.Data.Parsec -import Unicode.General.GeneralCategory +import UnicodeData -open Lean Unicode Xml Parser Parsec DocGen4.Process +open Lean Xml Parser Parsec DocGen4.Process namespace DocGen4 namespace Output @@ -55,9 +55,13 @@ partial def xmlGetHeadingId (el : Xml.Element) : String := |>.filter (!·.isEmpty) |> replacement.intercalate unicodeToDrop (c : Char) : Bool := - charInGeneralCategory c GeneralCategory.punctuation || - charInGeneralCategory c GeneralCategory.separator || - charInGeneralCategory c GeneralCategory.other + let generalCategory := Unicode.getGeneralCategory c + let cats := [ + Unicode.GeneralCategory.P, -- punctuation + Unicode.GeneralCategory.S, -- separator + Unicode.GeneralCategory.C -- other + ] + cats.elem generalCategory /-- This function try to find the given name, both globally and in current module. @@ -175,8 +179,13 @@ def autoLink (el : Element) : HtmlM Element := do | none => return [Content.Character s] unicodeToSplit (c : Char) : Bool := - charInGeneralCategory c GeneralCategory.separator || - charInGeneralCategory c GeneralCategory.other + let generalCategory := Unicode.getGeneralCategory c + let cats := [ + Unicode.GeneralCategory.S, -- separator + Unicode.GeneralCategory.C -- other + ] + cats.elem generalCategory + /-- Core function of modifying the cmark rendered docstring html. -/ partial def modifyElement (element : Element) : HtmlM Element := match element with diff --git a/lake-manifest.json b/lake-manifest.json index 96b9f31..024374b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -10,7 +10,7 @@ {"git": {"url": "https://github.com/leanprover/lake", "subDir?": null, - "rev": "c2c609b37f200b2c7b59dfcac4eefebd909295e3", + "rev": "f59328e3d9b23f0266e40ceb31cb4353d9bf0dae", "name": "lake", "inputRev?": "master"}}, {"git": @@ -26,8 +26,8 @@ "name": "leanInk", "inputRev?": "doc-gen"}}, {"git": - {"url": "https://github.com/xubaiw/Unicode.lean", + {"url": "https://github.com/fgdorais/UnicodeData", "subDir?": null, - "rev": "6dd6ae3a3839c8350a91876b090eda85cf538d1d", - "name": "Unicode", + "rev": "ece7fa88d13ae92b670e46035119bab89e5225df", + "name": "UnicodeData", "inputRev?": "main"}}]} diff --git a/lakefile.lean b/lakefile.lean index f558b8b..a718390 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -14,8 +14,8 @@ lean_exe «doc-gen4» { require CMark from git "https://github.com/xubaiw/CMark.lean" @ "main" -require Unicode from git - "https://github.com/xubaiw/Unicode.lean" @ "main" +require UnicodeData from git + "https://github.com/fgdorais/UnicodeData" @ "main" require Cli from git "https://github.com/mhuisi/lean4-cli" @ "nightly"