search

digama0 / mm0

Metamath Zero specification language
Creative Commons Zero v1.0 Universal
315 stars 40 forks source link

update mm1 delim docs, extension display name #31

Closed ammkrn closed 4 years ago

ammkrn commented 4 years ago

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 like Error at line 1 column 30: Parse error: TokFormula " ) } , ", so I may have been wrong in insinuating that this is a change from mm0.

digama0 commented 4 years ago

The LeftRight delimiter option is actually a change to the MM0 syntax, which is inherited by MM1. mm0-hs is just out of date here.

digama0 commented 4 years ago

The first part of this PR was merged in da5c965