Skip to content

editor: Support separate Claim $this is an editor editors#268

Merged
osnr merged 2 commits into
mainfrom
osnr/external-editor
Jun 4, 2026
Merged

editor: Support separate Claim $this is an editor editors#268
osnr merged 2 commits into
mainfrom
osnr/external-editor

Conversation

@osnr
Copy link
Copy Markdown
Collaborator

@osnr osnr commented Jun 1, 2026

Write a program that says Claim $this is an editor.

Now point a keyboard at that editor and point that editor at another program P. You can view and edit the code of P from the editor, so you can avoid weird overlaps of printed-code with edit-code. Sort of a hack -- we should think about how to show page margins and maybe zoom in and out without changing text scale -- but useful for now.

IMG_5487

@osnr osnr requested review from audreymgu and cwervo June 1, 2026 22:51
Copy link
Copy Markdown
Collaborator

@audreymgu audreymgu left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM! Also cool to look a bit more into how the editor works :)

@audreymgu audreymgu linked an issue Jun 4, 2026 that may be closed by this pull request
@osnr osnr merged commit 8d5ae3d into main Jun 4, 2026
@osnr osnr deleted the osnr/external-editor branch June 4, 2026 04:08
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.

Editor window size is too small when program size is reduced

2 participants