Function application should take precedence over continuing an `open`

[gebner]

import Something
open Something

something " 123 " -- 123 is colored as a number, but should be a string

[Julian]

Thanks! You're going to find quite a few issues, there still are some very basic things wrong with the parser -- including ones that mean it takes ridiculous amounts of time to generate at the minute... My best idea so far was just trying to get to the point where I parse advent-of-lean4 or now mathlib4 without errors, which I'm still not there yet on.

But please do file as many of these as you find!

[gebner]

I did not expect a complete grammar---the lean.nvim readme was pretty clear that this is experimental.

Errors are fine as well; the grammar in the vscode extension also has lots of corner cases that are incorrect. I don't mind if a keyword is not highlighted. It's only an issue if an occurrence of some unsupported syntax causes the rest of the file to be highlighted incorrectly (as in this issue and #4).

[Julian]

I looked at this quickly, it's a bit annoying at the minute -- this is being misparsed as

open <identifier>
<another identifier>

which is why the formatting is off, and to fix that I think is because I have precedence for application totally wrong, but it will take a bit of refactoring to fix.

The other ones I haven't looked at yet but may be easier.

[gebner]

This is indeed super ambiguous, the following is a valid three-line long open statement:

namespace something end something -- we need to define the namespace first

open Lean

something -- still part of the open statement :raised_eyebrow: 

[Julian]

Yeah :/