Repository navigation
Add inline SVG and iframe to the typed HTML - #1
Merged
Merged
Conversation
New content category Ctx.svg with tags svg, g, circle, text and SVG's a, plus iframe and the attributes they need (viewbox, cx, cy, r, x, y, fill, stroke, loading, crossorigin). SVG elements are never void so a circle closes explicitly. HTML and SVG both have an a tag, so the parser looks tag names up by category (Tag.ofNameIn?); the round-trip proof is unchanged except for supplying the category from the placement witness. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds inline SVG and
iframeto the typed HTML, so a site can draw diagrams and embed documents without leaving the DSL. Needed by maxvonhippel/FMxAI#4, which renders a proven-correct map as static SVG.What changed
Ctx.svg, with tagssvg(flow content, SVG children),g,circle,text(svgText, phrasing children) and SVG'sa(svgA), plusiframe. SVG elements are never void: in an HTML document a<circle>without a closing tag would swallow its siblings, so they render with explicit closing tags.viewbox(emitted lowercase; the HTML parser's SVG attribute adjustment restoresviewBox),cx,cy,r,x,y,fill,stroke, plusloadingandcrossorigin.atag, so the parser now looks tag names up by category:Tag.ofNameIn? c s, withTag.PlacesInas the side condition of the inverse lemma.parseNode_elgets the category from its placement witness (placeEl_placesIn); nothing else in the round-trip proof changes.Tag.ofNameIn?on bothas, a document with a map that round-trips, and type-level negatives (SVGais not flow content; text is not SVG content).scripts/check.shpasses: build, tests, axiom audit, escape-hatch audit, leanchecker.🤖 Generated with Claude Code