search

edwinb / idris2-vim

Vim mode for Idris 2
75 stars 26 forks source link

Fix positional error mentioned in #19 #20

Open WizardOfMenlo opened 3 years ago

WizardOfMenlo commented 3 years ago

Apparently, the ordering of the command arguments was giving issue to some users (me included) as detailed in #19 . Not sure why this is needed, as the help for idris2 seems to suggest to have [options] [input file], but apparently this is the case.

BorisNikulin commented 3 years ago

This sort of fixes it? I applied the patch manually and observed the plugin working more than before but not as I thought it would work with in place editing, such as writing in the cases on case split.

When using the plugin most commands had no output or in place edits. However, when manually pulling up the response window with \i some commands produced output. Namely \c and \mc with the same output of Strangely \d for docs , \t for type of, and \p for proof search also returns that.

After putting the function case equation back and thus satisfying the type checker, there is no output in the response window at all from the commands tried above.

\r for loading the file into the REPL (via vim terminal? or idris2 IDE mode?) still has the file not found problem.