From f09772960f0a2023a75822c4726db03c89a77b57 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 21 Mar 2024 08:57:17 +0100 Subject: [PATCH] fix: don't render all branches of choice nodes --- src/highlighting/SubVerso/Highlighting/Code.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/highlighting/SubVerso/Highlighting/Code.lean b/src/highlighting/SubVerso/Highlighting/Code.lean index 4898f01..716bdbd 100644 --- a/src/highlighting/SubVerso/Highlighting/Code.lean +++ b/src/highlighting/SubVerso/Highlighting/Code.lean @@ -592,6 +592,13 @@ partial def highlight' (ids : HashMap Lsp.RefIdent Lsp.RefIdent) (trees : Persis | _, _ => highlight' ids trees dot highlight' ids trees name + | .node _ `choice alts => + -- Arbitrarily select one of the alternatives found by the parser. Otherwise, quotations of + -- let-bindings with antiquotations as the bound variable leads to doubled bound variables, + -- because the parser emits a choice node in the quotation. And it's never correct to show + -- both alternatives! + if h : alts.size > 0 then + highlight' ids trees alts[0] | stx@(.node _ k children) => let pos := stx.getPos? for child in children do