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

Merge remote-tracking branch 'alexjbest/only-linkify-lean' into only-linkify-lean

main
Henrik 2023-09-09 23:26:00 +02:00
parent 13fb60f8a3 6137c9b300
commit 3c80369cca
1 changed files with 4 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
DocGen4/Output/DocString.lean
View File

@ -22,7 +22,7 @@ namespace Output
splitAroundAux s p b (s.next i) r splitAroundAux s p b (s.next i) r
/-- /--
Similar to `Stirng.split` in Lean core, but keeps the separater. Similar to `String.split` in Lean core, but keeps the separater.
e.g. `splitAround "a,b,c" (fun c => c = ',') = ["a", ",", "b", ",", "c"]` e.g. `splitAround "a,b,c" (fun c => c = ',') = ["a", ",", "b", ",", "c"]`
-/ -/
def splitAround (s : String) (p : Char → Bool) : List String := splitAroundAux s p 0 0 [] def splitAround (s : String) (p : Char → Bool) : List String := splitAroundAux s p 0 0 []
@ -195,7 +195,9 @@ partial def modifyElement (element : Element) : HtmlM Element :=
else if name = "a" then else if name = "a" then
extendAnchor el extendAnchor el
-- auto link for inline <code></code> -- auto link for inline <code></code>
else if name = "code" then else if name = "code" ∧
-- don't linkify code blocks explicitly tagged with a language other than lean
(((attrs.find? "class").getD "").splitOn.all (fun s => s == "language-lean" || !s.startsWith "language-")) then
autoLink el autoLink el
-- recursively modify -- recursively modify
else else