Commit 1ff3c89b authored by Manu Beffara's avatar Manu Beffara
Browse files

Support coqtopide as IDE slave command

This is required for Coq version 8.9.0. The previous command 'coqtop
-ideslave' is still supported as a second choice for compatibility.
parent d52710c6
......@@ -12,7 +12,7 @@ Requirements
Coq-au-Vim requires
- Vim version 8
- Coq version 8.6 or 8.7
- Coq version 8.6 or above
Prior versions of Vim will not be supported because version 8 is the one that
introduces asynchronous communication with external tools. Prior versions of
......@@ -499,13 +499,48 @@ endfunction
" Start the job for coqtop.
" When starting the toplevel, the actual command to run is not always the
" same, depending on versions: starting with Coq 8.9.0, we have to call
" 'coqidetop', while prior versions required 'coqtop -ideslave'. We handle
" this by trying each command successively until one succeeds. We detect
" success by checking if a call to the 'About' command did succeed before the
" job terminated.
function s:coq.start_job ()
if has_key(self, 'job') && !empty(self.job)
call self.stop_job()
let self.job_commands = [ 'coqidetop', 'coqtop -ideslave' ]
call self.try_start(v:none, v:none)
function s:coq.try_start (job, status)
if has_key(self, 'protocol')
" The job exited after successful initialisation.
if has_key(self, 'job')
" We are re-starting a job.
if empty(self.job)
call self.log('j', "failed")
call self.stop_job()
let cmd = 'coqtop -ideslave -main-channel stdfds -async-proofs on'
if empty(self.job_commands)
" All possible commands were tried without success.
call self.goals.close()
call self.infos.close()
echohl WarningMsg
echomsg "No Coq toplevel was found"
echohl None
" Try to start using the next potential command.
let cmd = remove(self.job_commands, 0) . ' -main-channel stdfds -async-proofs on'
call self.log('j', "start", cmd)
let self.job = job_start(cmd, {'mode': 'raw', 'out_cb': self.callback})
let self.job = job_start(cmd,
\ {'mode': 'raw', 'out_cb': self.callback, 'exit_cb': self.try_start})
let = job_getchannel(self.job)
call self.log('j', "started", self.job,
let self.xml_stack = []
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment