From 58fcc5d4680676e3df4fba160a712ecc8fe2b3e8 Mon Sep 17 00:00:00 2001 From: "Alex J. Best" Date: Sat, 5 Nov 2022 18:18:16 +0100 Subject: [PATCH] only linkify lean code --- DocGen4/Output/DocString.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index a4128bf..2238cc3 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -22,7 +22,7 @@ namespace Output 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"]` -/ 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 extendAnchor el -- auto link for inline - else if name = "code" then + else if name = "code" ∧ attrs.contains "language-lean" then autoLink el -- recursively modify else