From cdf98c40f1d72484ee2235e6c1ad55424e85b029 Mon Sep 17 00:00:00 2001
From: Lazare-42 <lazare@meetingbaas.com>
Date: Mon, 15 Jun 2026 10:54:14 +0200
Subject: [PATCH] fix(idrx): allow iframe attributes in markup validator

The idrx view macro validates element attributes against
knownHtmlAttributes when checkMarkup is on (the default in
inline/production mode). The iframe-specific attributes sandbox,
allow, allowfullscreen and srcdoc were missing from the list, so a
literal <iframe> with sandbox/allow attributes was rejected during
elaboration.

Because the rejection surfaces as a macro failure, it rendered as a
cryptic "Mismatch between String -> Elab Html and Elab ?scriptTy"
error rather than an "unknown attribute" message. Dev-runtime mode
skips the macro/validation entirely, which is why only production
builds tripped on it.

Fixes vcombey/iwf#2.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 libs/idris-html/src/Iwf/Html.idr | 1 +
 1 file changed, 1 insertion(+)

diff --git a/libs/idris-html/src/Iwf/Html.idr b/libs/idris-html/src/Iwf/Html.idr
index 052af23..10b50d1 100644
--- a/libs/idris-html/src/Iwf/Html.idr
+++ b/libs/idris-html/src/Iwf/Html.idr
@@ -1149,6 +1149,7 @@ knownHtmlAttributes =
   , "itemscope", "itemtype", "lang", "popover", "spellcheck", "translate"
   , "href", "target", "rel", "download", "hreflang", "media", "ping", "referrerpolicy"
   , "src", "srcset", "sizes", "alt", "width", "height", "loading", "decoding"
+  , "sandbox", "allow", "allowfullscreen", "srcdoc"
   , "type", "name", "value", "placeholder", "disabled", "checked", "readonly", "required"
   , "multiple", "selected", "autocomplete", "autoplay", "controls", "loop", "muted", "playsinline"
   , "action", "method", "enctype", "novalidate", "for", "form", "min", "max", "step", "pattern"