code2rocq/crocq
code2rocq/crocq
Watch
3
2
Fork
You've already forked crocq
 0
Code Issues 18 Pull requests 3 Projects 1 Releases 1 Packages 2 Activity Actions

Dedent inline clause bodies before writing them #84

Merged
marfavi merged 3 commits from fix/inline-clause-whitespace into main 2026-10-29 14:15:18 +01:00
Conversation 2 Commits 3 Files changed 3 +74 -4
marfavi commented 2026-10-28 14:50:51 +01:00
Owner

Fixes #76

Bodies indented inside the C annotation no longer leak that indentation into the proof document.

Fixes #76 Bodies indented inside the C annotation no longer leak that indentation into the proof document.
Dedent inline clause bodies before writing them (#76)
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 1m7s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 2m39s
Details
5476289b13
michael requested changes 2026-10-29 10:54:06 +01:00
Dismissed
extension/src/inlineClauseBody.ts Outdated
@ -14,0 +15,4 @@
/** Removes the indentation shared by every line. */
function dedent(body: string): string {
const lines = body.replace(/^[ \t]*\r?\n/, '').split(/\r?\n/);
while (lines.length > 0 && lines[lines.length - 1]?.trim() === '') {
michael commented 2026-10-29 10:53:47 +01:00
Owner

why are empty lines being filtered away 3 times in this one method?

on this line, line 22 and line 37

why are empty lines being filtered away 3 times in this one method? on this line, line 22 and line 37
marfavi marked this conversation as resolved
marfavi referenced this pull request from a commit 2026-10-29 14:04:07 +01:00
Handle inline clause blank lines once 
# Conflicts:
#	examples/sumarray/sumarray.c
Handle inline clause blank lines once
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 45s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 1m54s
Details
6e6dba0126 
Drop surrounding blank lines with trimming and ignore interior blank lines only when measuring the common indentation, instead of filtering empty lines three times.

Stop trimming the dedented body as well: that removed indentation which was intentionally deeper than the common prefix.

Addresses review feedback on #84.
marfavi scheduled this pull request to auto merge when all checks succeed 2026-10-29 14:07:01 +01:00
michael approved these changes 2026-10-29 14:15:14 +01:00
marfavi deleted branch fix/inline-clause-whitespace 2026-10-29 14:15:18 +01:00
Sign in to join this conversation.
Reviewers
No reviewers
michael
Labels
Clear labels   
blocked
should wait for another issue to be addressed

  
bug

   
priority!

   
quick-pick
No labels
blocked
bug
priority!
quick-pick
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
2 participants
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference
code2rocq/crocq!84
No description provided.