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

only linkify lean code

main
Alex J. Best 2022-11-05 18:18:16 +01:00
parent 6c8b79a539
commit 58fcc5d468
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
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" (λ c => c = ',') = ["a", ",", "b", ",", "c"]` e.g. `splitAround "a,b,c" (λ 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 []
@ -188,7 +188,7 @@ 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" ∧ attrs.contains "language-lean" then
autoLink el autoLink el
-- recursively modify -- recursively modify
else else