doc: update manual (#650)

Author: mhuisi

vscode-lean4/manual/manual.md

@@ -259,7 +259,7 @@ The InfoView is subdivided into several sections, most of which are only display
 1. **Expected type**. If the text cursor is positioned in a Lean term, the InfoView will display the current expected type at the position of the cursor. 
 1. **Widget sections**. Widgets may add arbitrary additional sections to the InfoView that are only displayed when the respective widget is active.
 1. **Messages**. If the text cursor is positioned on a line of the span of a [diagnostic](#errors-warnings-and-information), an interactive variant of the diagnostic is displayed. Disabling the 'Lean 4 > Infoview: All Errors On Line' option will only display errors that are to the right of the text cursor.
-1. **All Messages**. Always displayed. Contains interactive variants of all [diagnostics](#errors-warnings-and-information) present in the file. Can be paused by clicking the 'Pause 'All Messages'' button in the top right of the section.
+1. **All Messages**. Always displayed. Contains interactive variants of all [diagnostics](#errors-warnings-and-information) present in the file, sorted by their proximity to the text cursor by default. Can be paused by clicking the 'Pause 'All Messages'' button in the top right of the section. The sort order can be changed by clicking the 'Sort by message location' button, also in the top right of the section. The default sort order can be changed by setting the 'Lean 4 > Infoview: Message Order' option.
 
 All sections can be collapsed by clicking on their title using the mouse, but the expected type and all messages sections can also be collapsed and uncollapsed using the ['Infoview: Toggle Expected Type'](command:lean4.infoView.toggleExpectedType) and ['Infoview: Toggle "All Messages"'](command:lean4.displayList) commands, respectively. The expected type section can also be collapsed by default using the 'Lean 4: Infoview > Show Expected Type' setting.