Skip to content

Make view and edit include docs automatically#6170

Merged
aryairani merged 8 commits intotrunkfrom
edit-docs
Feb 12, 2026
Merged

Make view and edit include docs automatically#6170
aryairani merged 8 commits intotrunkfrom
edit-docs

Conversation

@mitchellwrosen
Copy link
Member

@mitchellwrosen mitchellwrosen commented Feb 11, 2026

Fixes #3707

Overview

This PR changes the behavior of view and edit to include docs automatically.

Screenshot 2026-02-11 at 12 47 45 PM

I initially endeavored to just change the behavior of edit as the ticket originally requests, but since view and edit share so much code, it was simpler to affect both. It's also useful to see docs of something that you just view, though I think an improvement might be to properly display the doc rather than just show the semi-pretty-printed version you currently get.

Test coverage

No new tests, but existing transcripts cover the change.

Loose ends

I realized rather late in development that the internal mechanism has an annoying corner case. The feature is currently implemented in two stages:

  1. Auto-expand the user's edit x y z to edit x y z x.doc y.doc z.doc
  2. Pair up docs with their terms/types.

However, I forgot about suffixification. There is some code related to essentially not displaying "stuff that the user didn't ask for" that I don't think would be necessary with the simpler idea of:

  1. Just do the search
  2. Do a follow-up query for those things' docs

I didn't think it was really worth eagerly reworking all of the internals, since this way works, it's just arguably not the best design.

@aryairani
Copy link
Contributor

Nice!

@aryairani aryairani added this pull request to the merge queue Feb 12, 2026
@aryairani aryairani removed this pull request from the merge queue due to a manual request Feb 12, 2026
@aryairani aryairani added this pull request to the merge queue Feb 12, 2026
@aryairani aryairani removed this pull request from the merge queue due to the queue being cleared Feb 12, 2026
@aryairani aryairani requested a review from a team as a code owner February 12, 2026 18:55
@aryairani aryairani added this pull request to the merge queue Feb 12, 2026
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to no response for status checks Feb 12, 2026
@aryairani aryairani added this pull request to the merge queue Feb 12, 2026
Merged via the queue into trunk with commit a0ef647 Feb 12, 2026
5 checks passed
@aryairani aryairani deleted the edit-docs branch February 12, 2026 23:11
@aryairani aryairani restored the edit-docs branch February 13, 2026 01:15
@aryairani aryairani deleted the edit-docs branch February 13, 2026 01:16
@ChrisPenner
Copy link
Member

Oh this is great!

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.

Edit should add docs to scratch file too

3 participants