structure Network.Wai.Middleware.Push.Referer.PushManager : Type

The push prediction manager. Thread-safe via IO.Ref.

• settings : PushSettings

  Settings.

• table : IO.Ref (LRU String (List PushPath))

  The push table: maps page paths to push resources.

def Network.Wai.Middleware.Push.Referer.PushManager.new (settings : PushSettings := { }) : IO PushManager

Create a new push manager.

Equations

• One or more equations did not get rendered due to their size.

def Network.Wai.Middleware.Push.Referer.PushManager.record (mgr : PushManager) (referer resource : String) : IO Unit

Record a resource request with its referer, updating the push table. When a resource is requested with a Referer header pointing to a page, we learn that the page needs that resource.

Equations

• One or more equations did not get rendered due to their size.

def Network.Wai.Middleware.Push.Referer.PushManager.getPushes (mgr : PushManager) (pagePath : String) : IO (List PushPath)

Get the list of resources to push for a given page path.

Equations

• mgr.getPushes pagePath = do let cache ← ST.Ref.get mgr.table match Network.Wai.Middleware.Push.Referer.LRU.lookup pagePath cache with | (result, snd) => pure (result.getD [])