update mm1 delim docs, extension display name #31
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The mm0 extension currently shows up in VScode's settings menu as "Example Configuration" instead of by name. Also the default executable path still points to mm0-hs, but it looks like cd66408 made mm0-rs the default server.
The doc change reflects the
Delimiter::LeftRight/Delimiter::Both
distinction, which I was confused by before looking at the parser. There's a bit of a discrepancy in that mm0-rs will accept mm0 files with two math-strings of delimiters, but mm0-hs will reject such a file with something likeError at line 1 column 30: Parse error: TokFormula " ) } , "
, so I may have been wrong in insinuating that this is a change from mm0.