-
Notifications
You must be signed in to change notification settings - Fork 428
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Align doc comments, support single line // comments #1800
base: master
Are you sure you want to change the base?
Conversation
@@ -0,0 +1,3 @@ | |||
module JustString : { | |||
include Map.S; // Comment eol include |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We will need to get the syntax highlighters to be updated. Vim should be good. But imagine if you had a brace or mismatched paren in a comment.
@@ -636,6 +636,11 @@ rule token = parse | |||
} | |||
|
|||
and enter_comment = parse | |||
| "//" ([^'\010']* newline as line) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@let-def Are there other kinds of newlines we need to watch out for (something like windows)?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It should be compatible with windows. However, it might break with MacOs 9 😿 .
Refactor the implementation of comments:
//
are accepted.Comments are now indented inside
Easy_format
, this enables a uniform treatment of all comments (normal comments, single line comments, doc comments, whether they are printed as atoms or attached to list wrappers).Hence the modifications to Easy_format.
pp_print_as
is used to trickFormat
to put newlines:pp_force_newline
forces a newline in the current box, while usingpp_print_as
with a size larger than the current margin puts the newline in the next box that receives content.To merge after #1799 .