From a8a2b8e0fb6dbe2621dc9ab8ee61edfa1c8af9b7 Mon Sep 17 00:00:00 2001 From: Krishna Padmasola Date: Sun, 17 Aug 2025 21:48:42 +0530 Subject: [PATCH 1/4] Add `toTex` support for `Manual.keywordOf` --- Manual/Meta/Syntax.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Manual/Meta/Syntax.lean b/Manual/Meta/Syntax.lean index e2a6e26e..092a1a94 100644 --- a/Manual/Meta/Syntax.lean +++ b/Manual/Meta/Syntax.lean @@ -125,7 +125,10 @@ def keywordOf : RoleExpander def keywordOf.descr : InlineDescr where traverse _ _ _ := do pure none - toTeX := none + toTeX := + some <| fun go _id _ content => do + pure <| .seq <| ← content.mapM fun b => do + pure <| .seq #[← go b, .raw "\n"] toHtml := open Verso.Output Html in some <| fun goI _ info content => do From 87c1888889671aa0c020b0438efc386eb12e7915 Mon Sep 17 00:00:00 2001 From: Krishna Padmasola Date: Mon, 18 Aug 2025 15:25:48 +0530 Subject: [PATCH 2/4] removed newline from TeX output chore: adapt to updated argument and flag syntax (#570) --- Manual/Meta/Syntax.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Manual/Meta/Syntax.lean b/Manual/Meta/Syntax.lean index 092a1a94..9ae2a955 100644 --- a/Manual/Meta/Syntax.lean +++ b/Manual/Meta/Syntax.lean @@ -126,9 +126,9 @@ def keywordOf.descr : InlineDescr where traverse _ _ _ := do pure none toTeX := - some <| fun go _id _ content => do + some <| fun goI _id _ content => do pure <| .seq <| ← content.mapM fun b => do - pure <| .seq #[← go b, .raw "\n"] + pure <| .seq #[← goI b] toHtml := open Verso.Output Html in some <| fun goI _ info content => do From a3cd727d882e0a40114dafb48674f62efcd9ba70 Mon Sep 17 00:00:00 2001 From: Krishna Padmasola Date: Mon, 18 Aug 2025 15:49:29 +0530 Subject: [PATCH 3/4] Fix merge issue From 8a65ca21f63609b39c6cd0a3d2a9a381457b7b97 Mon Sep 17 00:00:00 2001 From: Krishna Padmasola Date: Mon, 18 Aug 2025 20:11:04 +0530 Subject: [PATCH 4/4] address review comment --- Manual/Meta/Syntax.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Manual/Meta/Syntax.lean b/Manual/Meta/Syntax.lean index 9ae2a955..743f702b 100644 --- a/Manual/Meta/Syntax.lean +++ b/Manual/Meta/Syntax.lean @@ -125,10 +125,7 @@ def keywordOf : RoleExpander def keywordOf.descr : InlineDescr where traverse _ _ _ := do pure none - toTeX := - some <| fun goI _id _ content => do - pure <| .seq <| ← content.mapM fun b => do - pure <| .seq #[← goI b] + toTeX := some fun goI _ _ content => content.mapM goI toHtml := open Verso.Output Html in some <| fun goI _ info content => do