Skip to content

Browser auto-reload; text script covers properties and implications - #424

Merged
ScriptRaccoon merged 4 commits into
mainfrom
text-script-and-refactor
Oct 12, 2026
Merged

ScriptRaccoon merged 4 commits into
mainfrom
text-script-and-refactor

Conversation

@ScriptRaccoon

@ScriptRaccoon ScriptRaccoon commented Oct 11, 2026 •

Copy link
Copy Markdown
Owner
  • While pnpm dev is running, the browser reloads automatically after db:update or db:text changes the database. This is done with a custom Vite plugin.
  • pnpm db:text now also updates properties (descriptions, nLab links), implication proofs, and more structure fields (alternative notations, comments, keywords, objects and morphisms of categories). With --watch, it also reacts to changes in property and implication files.
  • The folders symmetric_monoidal_category_properties/ and symmetric_monoidal_category_implications/ are renamed to symmetric_monoidal_category-properties/ and symmetric_monoidal_category-implications/, consistent with the other types.
  • The seed script is refactored; the generated data is unchanged.

How it looks like (Video)

@ScriptRaccoon ScriptRaccoon added feature features of the application visible to users as well as features for maintainers refactor changes that do not change behavior, but improve the code labels Oct 11, 2026
@ScriptRaccoon ScriptRaccoon changed the title Text script and refactor Text script covers properties and implications; browser auto-reload Oct 11, 2026
@ScriptRaccoon
ScriptRaccoon force-pushed the text-script-and-refactor branch from 937c34a to d744b10 Compare October 11, 2026 18:43
@ScriptRaccoon ScriptRaccoon changed the title Text script covers properties and implications; browser auto-reload Browser auto-reload; text script covers properties and implications Oct 11, 2026
@ScriptRaccoon

Copy link
Copy Markdown
Owner Author

@dschepler FYI, I think the browser auto-reload will be very convenient.

@ScriptRaccoon
ScriptRaccoon merged commit dea1a0b into main Oct 12, 2026
4 checks passed
@ScriptRaccoon
ScriptRaccoon deleted the text-script-and-refactor branch October 12, 2026 05:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

feature features of the application visible to users as well as features for maintainers refactor changes that do not change behavior, but improve the code

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant