gterzian

-------------------------- MODULE CanvasRendering --------------------------
EXTENDS FiniteSets, Integers, Sequences
VARIABLES images_updated, display_lists_applied, 
           compositor_messages, canvas_state,
           pending_display_list
CONSTANT N
----------------------------------------------------------------------------

Messages == {"DISPLAY_LIST", "UPDATE_IMAGE"}

gterzian

-------------------------- MODULE CanvasRenderingBlocking --------------------------
EXTENDS FiniteSets, Integers, Sequences
VARIABLES images_updated, display_lists_applied, compositor_messages, canvas_state
CONSTANT N
----------------------------------------------------------------------------

Messages == {"DISPLAY_LIST", "UPDATE_IMAGE"}

CanvasState == {"PENDING", "UPDATED"}

gterzian

-------------------------- MODULE CanvasRenderingBroken --------------------------
EXTENDS FiniteSets, Integers, Sequences
VARIABLES images_updated, display_lists_applied, compositor_messages
----------------------------------------------------------------------------

Messages == {"DISPLAY_LIST", "UPDATE_IMAGE"}

ReadyToApplyDisplayList == images_updated = display_lists_applied + 1
ImageUpdatedAndDisplayListApplied == images_updated = display_lists_applied

gterzian

How to work on a Web API

Part 1: Basic Setup of a Web API

1. Read-up on the relevant spec.
2. Add .webidl file(s) in this folder for each interface that you want to implement. If one already exists, you want to add the missing parts to it.
3. For each interface, this will generate a trait named {interface_name}Methods, accessible via use crate::dom::bindings::codegen::Bindings::{interface_name}Binding.
4. Use this trait by:
   • Adding a matching struct, using #[dom_struct]

• Adding methods with todo! bodies.

gterzian

How to work on a Web API with the assistance of Copilot

Part 1: Basic Setup of a Web API

1. Read-up on the relevant spec.
2. Add .webidl file(s) in this folder for each interface that you want to implement. If one already exists, you want to add the missing parts to it.
3. For each interface, this will generate a trait named {interface_name}Methods, accessible via use crate::dom::bindings::codegen::Bindings::{interface_name}Binding.
4. Use this trait by:
   • Adding a matching struct, using #[dom_struct]

• Adding methods with todo! bodies.

gterzian

ServiceWorker implementation items:

Interfaces

Client Context

• ServiceWorker
• ServiceWorkerRegistration
• ServiceWorkerContainer
• NavigationPreloadManager

gterzian

---------------------------- MODULE Presentation ----------------------------
EXTENDS FiniteSets, Integers, Sequences
VARIABLES next_presentation_id, current_presentation_id, pending_ids
CONSTANT N
----------------------------------------------------------------------------

TypeOk == /\ next_presentation_id \in Int
          /\ current_presentation_id \in Int
          /\ pending_ids \in Seq(Int)
  

gterzian

Conversation in the context of servo/servo#32898

In this issue, how can I do the " Handle fufillment of pull algo promise" part?

The details of issue #32898 in the servo/servo repository include a task to handle the fulfillment of the pull algorithm promise.

Steps to handle the fulfillment:

1. Locate the Relevant Code: The task is related to the PullAlgorithmFulfillmentHandler in the ReadableStreamDefaultController. You can find it in the file readablestream.rs.

gterzian

----------------------------- MODULE RafDelivery -----------------------------
EXTENDS FiniteSets, Naturals
VARIABLES raf_requested, tick_received
CONSTANT N
----------------------------------------------------------------------------
Pipeline == 0..N

TypeOk == /\ raf_requested \in [Pipeline -> BOOLEAN]
          /\ tick_received \in BOOLEAN
  

gterzian

----------------------------- MODULE RafBroken -----------------------------
EXTENDS FiniteSets, Naturals
VARIABLES raf_requested, tick_received
CONSTANT N
----------------------------------------------------------------------------
Pipeline == 0..N

TypeOk == /\ raf_requested \in [Pipeline -> BOOLEAN]
          /\ tick_received \in [Pipeline -> BOOLEAN]