Lines of tildes in comments screw up Lean parsing in this plugin

[kevinsullivan]

This works fine:

/-
~~
-/
def x := 1

Add one more tilde and important stuff breaks.

/-
~~~
-/
def x := 1  -- code highlighting no longer works and other stuff breaks, too.

This is a problem because lines of tildes are used as subsection markup in RestructuredText documents, which J. Avigad and others are using to format Lean files as presentable documents.

This is a consequential bug, and given the simplicity of the test cases here, should be pretty easy to track down.

Thank you, Kevin Sullivan University of Virginia