Skip to content

refactor: define HTML media interfaces locally - #307

Open
jderochervlk wants to merge 1 commit into
codex/html-embedded-resourcesfrom
codex/html-media-elements
Open

refactor: define HTML media interfaces locally#307
jderochervlk wants to merge 1 commit into
codex/html-embedded-resourcesfrom
codex/html-media-elements

Conversation

@jderochervlk

@jderochervlk jderochervlk commented Aug 3, 2026

Copy link
Copy Markdown
Collaborator

Tracking issue: #342

Summary

  • define the shared HTML media-element record in DomHTMLMediaElement
  • move audio, video, track, time-range, and text-track types beside their APIs
  • add the public MediaError and VideoPlaybackQuality modules
  • update media bindings to use the locally owned types

Temporary state

  • the equivalent aggregate media definitions remain in DOM/DomTypes during this layer
  • refactor: remove DOM compatibility types #310 removes those copies once the remaining consumers have migrated
  • the current physical placement under the broad DOM folder is temporary; the follow-up Option 5 stack separates HTML and Media folder features

Review focus

  • inheritance and shared fields in DomHTMLMediaElement
  • video callback, playback-quality, track, and error signatures

Verification

  • npm run build
  • npm test
  • npm run format:check

Copy link
Copy Markdown
Collaborator Author

@codex

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 18300fd28a

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

Comment thread src/DOM/HTMLVideoElement.res
Comment thread src/DOM/VideoPlaybackQuality.res
@jderochervlk
jderochervlk force-pushed the codex/html-media-elements branch 4 times, most recently from e5c6ae3 to 4500575 Compare August 5, 2026 12:34
@jderochervlk
jderochervlk force-pushed the codex/html-media-elements branch 2 times, most recently from 681c058 to 1cf7480 Compare August 5, 2026 13:57
@jderochervlk
jderochervlk force-pushed the codex/html-media-elements branch from 1cf7480 to 8eca249 Compare August 5, 2026 14:00
@jderochervlk
jderochervlk force-pushed the codex/html-media-elements branch from 8eca249 to 6dcfd49 Compare August 5, 2026 15:08
@jderochervlk
jderochervlk force-pushed the codex/html-media-elements branch from 6dcfd49 to c08d80c Compare August 5, 2026 17:39
@jderochervlk
jderochervlk force-pushed the codex/html-media-elements branch from c08d80c to 04df2f0 Compare August 6, 2026 14:52
@jderochervlk
jderochervlk force-pushed the codex/html-media-elements branch from 04df2f0 to a9aaa5f Compare August 6, 2026 14:58
@jderochervlk
jderochervlk force-pushed the codex/html-media-elements branch from a9aaa5f to 3883290 Compare August 6, 2026 15:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant