Commit 213d6268 authored by Adam Matoušek's avatar Adam Matoušek
Browse files

Support simple _CoqProject files.

E.g. these from the Software Foundations books (at least the first two).
parent 1ff3c89b
......@@ -488,6 +488,30 @@ let s:coq = { }
function s:coq.log (...)
" == _CoqProject file loading == {{{2
" _CoqProject is the default name of the file containing local configuration to
" be passed to coqtop. Lines starting with a pound sign (#) are ignored.
" The file is only parsed when g:coq_options contains 'p'. If g:coq_project_file
" exists, its contents is used as the project file name instead of the default
" '_CoqProject'
function s:coq.load_coqproject ()
let self.coqproject_opts = ''
if !self.options.p
let fname = exists('g:coq_project_file') ? g:coq_project_file : '_CoqProject'
if ! filereadable(fname)
for line in readfile(fname)
if line !~ '^\s*#'
let self.coqproject_opts .= ' ' . trim(line)
" == Job management and basic communication == {{{2
" Coqtop interacts asynchronously by exchanging messages as XML nodes. We use
......@@ -537,7 +561,8 @@ function s:coq.try_start (job, status)
" Try to start using the next potential command.
let cmd = remove(self.job_commands, 0) . ' -main-channel stdfds -async-proofs on'
let cmd = remove(self.job_commands, 0) . ' -main-channel stdfds -async-proofs on ' . self.coqproject_opts
let cmd = trim(cmd) "trailing whitespace seems to break job_start
call self.log('j', "start", cmd)
let self.job = job_start(cmd,
\ {'mode': 'raw', 'out_cb': self.callback, 'exit_cb': self.try_start})
......@@ -1376,9 +1401,9 @@ function s:coq.create ()
let new.buffer = bufnr("")
let new.debugging = exists('g:coq_debug')
let options = exists('g:coq_options') ? g:coq_options : 'h'
let options = exists('g:coq_options') ? g:coq_options : 'hp'
let new.options = {}
for opt in ['h', 's']
for opt in ['h', 's', 'p']
let new.options[opt] = stridx(options, opt) >= 0
......@@ -1392,6 +1417,7 @@ function s:coq.create ()
call win_gotoid(winid)
call new.load_coqproject()
call new.start_job()
call new.call_about(new.start_version, {})
return new
......@@ -200,12 +200,14 @@ will set the option 'Printing Implicit' as boolean to true.
Options for the Coq interaction plugin are read from the global variable
variable *g:coq_options* on startup. This variable is expected to be string,
the presence of each letter below will activate the associated option. The
default value is "h".
default value is "hp".
letter option~
h highlight active regions of the buffer according to their state, the
way CoqIDE does, see |coq-highlight| for details
s mark active regions using signs
p use Coq options from the "_CoqProject" file. You can use
*g:coq_project_file* to specify an alternative file name.
Folding can be activated by setting 'foldmethod' to expr, see |coq-folding|.
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