r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

refactor: switch to maintained unicode lib

main
Henrik Böving 2023-03-11 18:06:13 +01:00
parent 720e1acf81
commit 5f59fbaac4
3 changed files with 22 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
DocGen4/Output/DocString.lean
View File

@ -1,9 +1,9 @@
import CMark import CMark
import DocGen4.Output.Template import DocGen4.Output.Template
import Lean.Data.Parsec 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 DocGen4
namespace Output namespace Output
@ -55,9 +55,13 @@ partial def xmlGetHeadingId (el : Xml.Element) : String :=
|>.filter (!·.isEmpty) |>.filter (!·.isEmpty)
|> replacement.intercalate |> replacement.intercalate
unicodeToDrop (c : Char) : Bool := unicodeToDrop (c : Char) : Bool :=
charInGeneralCategory c GeneralCategory.punctuation || let generalCategory := Unicode.getGeneralCategory c
charInGeneralCategory c GeneralCategory.separator || let cats := [
charInGeneralCategory c GeneralCategory.other 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. 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 => | none =>
return [Content.Character s] return [Content.Character s]
unicodeToSplit (c : Char) : Bool := unicodeToSplit (c : Char) : Bool :=
charInGeneralCategory c GeneralCategory.separator || let generalCategory := Unicode.getGeneralCategory c
charInGeneralCategory c GeneralCategory.other let cats := [
Unicode.GeneralCategory.S, -- separator
Unicode.GeneralCategory.C -- other
]
cats.elem generalCategory
/-- Core function of modifying the cmark rendered docstring html. -/ /-- Core function of modifying the cmark rendered docstring html. -/
partial def modifyElement (element : Element) : HtmlM Element := partial def modifyElement (element : Element) : HtmlM Element :=
match element with match element with

8
lake-manifest.json
View File

@ -10,7 +10,7 @@
{"git": {"git":
{"url": "https://github.com/leanprover/lake", {"url": "https://github.com/leanprover/lake",
"subDir?": null, "subDir?": null,
"rev": "c2c609b37f200b2c7b59dfcac4eefebd909295e3", "rev": "f59328e3d9b23f0266e40ceb31cb4353d9bf0dae",
"name": "lake", "name": "lake",
"inputRev?": "master"}}, "inputRev?": "master"}},
{"git": {"git":
@ -26,8 +26,8 @@
"name": "leanInk", "name": "leanInk",
"inputRev?": "doc-gen"}}, "inputRev?": "doc-gen"}},
{"git": {"git":
{"url": "https://github.com/xubaiw/Unicode.lean", {"url": "https://github.com/fgdorais/UnicodeData",
"subDir?": null, "subDir?": null,
"rev": "6dd6ae3a3839c8350a91876b090eda85cf538d1d", "rev": "ece7fa88d13ae92b670e46035119bab89e5225df",
"name": "Unicode", "name": "UnicodeData",
"inputRev?": "main"}}]} "inputRev?": "main"}}]}

4
lakefile.lean
View File

@ -14,8 +14,8 @@ lean_exe «doc-gen4» {
require CMark from git require CMark from git
"https://github.com/xubaiw/CMark.lean" @ "main" "https://github.com/xubaiw/CMark.lean" @ "main"
require Unicode from git require UnicodeData from git
"https://github.com/xubaiw/Unicode.lean" @ "main" "https://github.com/fgdorais/UnicodeData" @ "main"
require Cli from git require Cli from git
"https://github.com/mhuisi/lean4-cli" @ "nightly" "https://github.com/mhuisi/lean4-cli" @ "nightly"