42 lines
1.6 KiB
MySQL
42 lines
1.6 KiB
MySQL
|
-- A GUI publication binds paused to its display epoch. Agent barrier changes
|
||
|
|
-- must therefore invalidate that agent's displays in the same transaction,
|
||
|
|
-- even when the writer does not use the API helper. Independent agents keep
|
||
|
|
-- their epochs. This is allocation, not a Runner barrier acknowledgement.
|
||
|
|
CREATE FUNCTION fence_agent_barrier_displays() RETURNS TRIGGER LANGUAGE plpgsql AS $$
|
||
|
|
DECLARE
|
||
|
|
target_bot TEXT;
|
||
|
|
was_paused BOOLEAN := FALSE;
|
||
|
|
is_paused BOOLEAN := FALSE;
|
||
|
|
BEGIN
|
||
|
|
IF TG_OP <> 'INSERT' THEN
|
||
|
|
target_bot := OLD.bot_id;
|
||
|
|
was_paused := OLD.paused;
|
||
|
|
END IF;
|
||
|
|
IF TG_OP <> 'DELETE' THEN
|
||
|
|
target_bot := NEW.bot_id;
|
||
|
|
is_paused := NEW.paused;
|
||
|
|
END IF;
|
||
|
|
-- A primary key move also removes the old bot's barrier.
|
||
|
|
IF TG_OP='UPDATE' AND NEW.bot_id IS DISTINCT FROM OLD.bot_id THEN
|
||
|
|
IF OLD.paused THEN
|
||
|
|
UPDATE computer_screens SET display_epoch=display_epoch+1
|
||
|
|
WHERE bot_id=OLD.bot_id;
|
||
|
|
END IF;
|
||
|
|
was_paused := FALSE;
|
||
|
|
END IF;
|
||
|
|
IF was_paused IS DISTINCT FROM is_paused THEN
|
||
|
|
UPDATE computer_screens SET display_epoch=display_epoch+1
|
||
|
|
WHERE bot_id=target_bot;
|
||
|
|
END IF;
|
||
|
|
RETURN NULL;
|
||
|
|
END
|
||
|
|
$$;
|
||
|
|
|
||
|
|
CREATE TRIGGER agent_barrier_display_epochs
|
||
|
|
AFTER INSERT OR UPDATE OR DELETE ON agent_mutation_barriers
|
||
|
|
FOR EACH ROW EXECUTE FUNCTION fence_agent_barrier_displays();
|
||
|
|
|
||
|
|
-- Existing paused rows may already have a published unpaused GUI epoch.
|
||
|
|
UPDATE computer_screens s SET display_epoch=s.display_epoch+1
|
||
|
|
WHERE EXISTS(SELECT 1 FROM agent_mutation_barriers b WHERE b.bot_id=s.bot_id AND b.paused);
|