🌐 US-Proxy
class="logged-out env-production page-responsive" style="word-wrap: break-word;" >
Skip to content

Re-enable paged output after a file event. - #6045

Merged
aryairani merged 3 commits into
trunkfrom
cp/fix-paging
Dec 11, 2025
Merged

Re-enable paged output after a file event.#6045
aryairani merged 3 commits into
trunkfrom
cp/fix-paging

Conversation

@ChrisPenner

@ChrisPenner ChrisPenner commented Dec 10, 2025

Copy link
Copy Markdown
Member

Overview

An interesting glitch from the Discord;
https://discord.com/channels/862108724948500490/1444704371295129741

User reported that after updating the scratch file the pager no longer worked;

Implementation approach and notes

Turns out an IORef was being disabled on every File Event, but was never being re-enabled.

I changed it so that whether an output is paged depends on the output message itself.

Interesting/controversial decisions

I considered a couple approaches (see commit history);

  • Easiest fix is to just set the IORef back on each new message type; but global state led to this bug in the first place, doesn't seem great.
  • Another option was to edit the notify of the Env before running each step
  • Use paging depending on the type of message we're printing

I went with the latter approach since it seems the most semantically correct to me, and is also the most flexible.

Test coverage

Tested manually; seems tough to add an automated test for this one

@ChrisPenner
ChrisPenner marked this pull request as ready for review December 10, 2025 21:44
@aryairani
aryairani merged commit 004fe25 into trunk Dec 11, 2025
31 checks passed
@aryairani
aryairani deleted the cp/fix-paging branch December 11, 2025 00:48
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.

2 participants