From 58fcc5d4680676e3df4fba160a712ecc8fe2b3e8 Mon Sep 17 00:00:00 2001 From: "Alex J. Best" Date: Sat, 5 Nov 2022 18:18:16 +0100 Subject: [PATCH 1/4] 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 From 07cb0ed1ccffa99136afb8caead78c7b6cc1b1a0 Mon Sep 17 00:00:00 2001 From: "Alex J. Best" Date: Sat, 5 Nov 2022 18:28:27 +0100 Subject: [PATCH 2/4] fix --- DocGen4/Output/DocString.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 2238cc3..f9f0e34 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -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" ∧ attrs.contains "language-lean" then + else if name = "code" ∧ attrs.find? "class" = "language-lean" then autoLink el -- recursively modify else From d62268b013b1d03fdafe96c1381c0effbdfd3ad1 Mon Sep 17 00:00:00 2001 From: "Alex J. Best" Date: Sat, 5 Nov 2022 18:46:20 +0100 Subject: [PATCH 3/4] better --- DocGen4/Output/DocString.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index f9f0e34..f813288 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -188,7 +188,9 @@ partial def modifyElement (element : Element) : HtmlM Element := else if name = "a" then extendAnchor el -- auto link for inline - else if name = "code" ∧ attrs.find? "class" = "language-lean" then + else if name = "code" ∧ + -- don't linkify code blocks explicitly tagged with a language other than lean + ((¬ attrs.contains "class") ∨ (((attrs.find? "class").getD "").splitOn).filter (fun s => s.startsWith "language-" ∧ s ≠ "language-lean") = []) then autoLink el -- recursively modify else From fc00a41ecb606b9ebde7eeca1d626c4914fba034 Mon Sep 17 00:00:00 2001 From: "Alex J. Best" Date: Sun, 6 Nov 2022 21:27:26 +0100 Subject: [PATCH 4/4] bool --- DocGen4/Output/DocString.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index f813288..e59f287 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -190,7 +190,7 @@ partial def modifyElement (element : Element) : HtmlM Element := -- auto link for inline else if name = "code" ∧ -- don't linkify code blocks explicitly tagged with a language other than lean - ((¬ attrs.contains "class") ∨ (((attrs.find? "class").getD "").splitOn).filter (fun s => s.startsWith "language-" ∧ s ≠ "language-lean") = []) then + (((attrs.find? "class").getD "").splitOn.all (fun s => s == "language-lean" || !s.startsWith "language-")) then autoLink el -- recursively modify else