You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: doc/odoc_for_authors.mld
+6-11Lines changed: 6 additions & 11 deletions
Original file line number
Diff line number
Diff line change
@@ -399,19 +399,14 @@ Odoc strips whitespace from the content of a codeblock, so that it contains only
399
399
]}
400
400
v}
401
401
402
-
In other words, [odoc]:
402
+
In other words, [odoc], in order:
403
403
{ol
404
-
{- Removes the first line if it contains only whitespace,}
405
-
{- Removes the last line if it contains only whitespace,}
406
-
{- Deindents as much as the opening curly brace's column. If there is
407
-
non-whitespace on the left of the box above, the content is deindented only as
408
-
much as it can without stripping non-whitespace, and a warning is raised.}}
404
+
{- Does not remove any content if [{\[] and [\]}] are on the same line.}
405
+
{- Removes the content of the line after [{\[] if it contains only whitespace.}
406
+
{- Removes the content of the line before [\]}] if it contains only whitespace.}
407
+
{- Removes spaces and tabs (counted as a single spaces) to reach the column of the opening curly brace of the [{\[] marker. If there is non-whitespace on the left of this column, the content is deindented only as much as it can without stripping non-whitespace, and a warning is raised.}}
409
408
410
-
Note that removal of lines are meant "including the newline character" (so,
411
-
nothing is removed if there is no newline character: [{[ content ]}] stays the
412
-
same, but so do [{[ ]}]).
413
-
414
-
Also, note that if point 1 above does not remove a line, the content of the code
409
+
Also, note that if point 2 above does not remove a line, the content of the code
415
410
block is considered as if starting at the upper [+] in the box above:
0 commit comments