search

FStarLang / VimFStar

A Vim mode for FStar
Vim License
24 stars 12 forks source link

Delete interactive functionality #21

Closed maxzinkus closed 4 years ago

maxzinkus commented 4 years ago

As this plugin is deprecated, nobody will maintain the somewhat buggy interactive stuff. Deleting this code fixes #14 and fixes #15, and preps the repo for long-term inclusion into vim-polyglot.

maxzinkus commented 4 years ago

Actually I may be able to do the port to handle —ide

ad-l commented 4 years ago

You're right that nobody is currently maintaining Vim interactive mode. There is some documentation on --id on the F* wiki https://github.com/FStarLang/FStar/wiki/Editor-support-for-F%2A