Autocompletion is too eager after in and with

[tchajed]

company-coq has special handling of in and with at the end of the line to avoid providing autocompletions when typing let and match constructs. F* has the same issue:

module Test

let _ = let foo = 1 in
        foo

let with_const = 1

let _ = match 1 with
        | 1 -> true

Typing the above will result in in being auto-completed to int upon hitting enter. Once with_const as been processed, with will auto-complete to with_const (in practice the problematic identifier for me is FStar.HyperStack.ST.with_frame).

[tchajed]

I'll give this a try at some point, given @cpitclaudel showed me the relevant company-coq code while writing https://github.com/cpitclaudel/company-coq/pull/165.

[cpitclaudel]

I'm +1 on doing this soon; it's a pain

[cpitclaudel]

Let me know if you need help

[cpitclaudel]

Any news on this?

[catalin-hritcu]

I concur that keywords should always take precedence over longer(!) names from the library. Without this autocompletion is so much a pain that I feel like just switching it off completely. In part this pain is also caused by the emacs mode taking over the enter key, while I use that for ending a line. Isn't enough to have tab for autocompletion; what's the rational for taking over enter? When I'm at the end of a line, do I really need to hit Ctrl+G or Esc-Esc-Esc to get rid of useless autocompletion before I can break a line?

[tchajed]

@cpitclaudel feel free to take this over, since I'm not doing anything in F* right now

[cpitclaudel]

I concur that keywords should always take precedence

I think we're all in violent agreement here.

over longer(!) names from the library.

Not sure what (!) means :/

Without this autocompletion is so much a pain that I feel like just switching it off completely.

There's a setting to turn autocompletion off in fstar-enabled-modules, which you can get to using M-x customize.

In part this pain is also caused by the emacs mode taking over the enter key, while I use that for ending a line.

That's easy to disable:

(with-eval-after-load 'company
  (define-key company-active-map [return] nil)
  (define-key company-active-map (kbd "RET") nil))

Isn't enough to have tab for autocompletion; what's the rational for taking over enter?

Tab doesn't do the same as ret. Other than this, I don't know: it's a company setting unchanged in fstar-mode (IOW, I didn't pick that default). See C-h v company-active-map.

When I'm at the end of a line, do I really need to hit Ctrl+G or Esc-Esc-Esc to get rid of useless autocompletion before I can break a line?

See above. Does that help?

[catalin-hritcu]

In part this pain is also caused by the emacs mode taking over the enter key, while I use that for ending a line.

That's easy to disable:

(with-eval-after-load 'company
  (define-key company-active-map [return] nil)
  (define-key company-active-map (kbd "RET") nil))

Awesome! Many thanks. Wouldn't making this be the default solve this issue?

Isn't enough to have tab for autocompletion; what's the rational for taking over enter?

Tab doesn't do the same as ret.

Interesting, so what's the difference?

[cpitclaudel]

Awesome! Many thanks. Wouldn't making this be the default solve this issue?

No, not really. For two reasons. First, because this behavior comes from a different package, and it's frowned upon in Emacs land to change another package's defaults (the rationale makes sense: many Emacs users use company with more than one language, and want it to behave consistently everywhere). Second, because (see below) you do need a key that does what RET currently does, and TAB isn't it.

Tab doesn't do the same as ret.

Interesting, so what's the difference?

Tab autocompletes the common prefix, like in the shell. So if you type FSt, tab will complete to FStar..

[catalin-hritcu]

Tab autocompletes the common prefix, like in the shell. So if you type FSt, tab will complete to FStar..

And how is this different from what Enter does?

[cpitclaudel]

RET completes the whole identifier.