Clément Pit-Claudel

The fix would be to refine the predicate that's used for picking headers to start on. Currently it checks for preceding blanks and being outside of a comment.

Does `import docutils` work in the terminal?

I use Ubuntu; I haven't written F* recently/ I suspect pip install docutils might be enough; it will install it globally.

Hm, how annoying. I don't want to silence the warnings permanently, but I'd be happy to help you disable them temporarily while in deadline mode. Add this to your .emacs:...

Do you get a lot of these warnings? I'd really really like to reproduce them. Can you enable fstar-mode debugging and try to get a repro?

Excellent, thanks. I'll look at this.

One more question: are you positive turning company off solves it? This will help me focus on one of the likely sources.

Can you add this to your .emacs (without the snippet I gave above)? ``` (require 'fstar-mode) (defun fstar-subp-company--async-meta (candidate callback) "Find type of CANDIDATE and pass it to CALLBACK." (cl-assert...

OK, thanks. One more thing to add: ``` (defun fstar-subp-company-backend (command &optional arg &rest _rest) "Company backend for F*. Candidates are provided by the F* subprocess. COMMAND, ARG, REST: see...

It does! How surprising. Hold on.