Commit 588794d3 authored by Manu Beffara's avatar Manu Beffara
Browse files

Use global variables for options.

parent ae9100a5
......@@ -478,7 +478,7 @@ endfunction
" - messages: a list of messages received as feedback
" For the initial state, the range is set to [[1,0], [1,0]].
"
" The options (as defined by b:coq_options) are stored in a field 'options'
" The options (as defined by g:coq_options) are stored in a field 'options'
" which is a dictionary mapping each option letter to its boolean value.
let s:coq = { }
......@@ -1314,9 +1314,9 @@ endfunction
function s:coq.create ()
let new = copy(self)
let new.buffer = bufnr("")
let new.debugging = exists('b:coq_debug')
let new.debugging = exists('g:coq_debug')
let options = exists('b:coq_options') ? b:coq_options : 'h'
let options = exists('g:coq_options') ? g:coq_options : 'h'
let new.options = {}
for opt in ['h', 's']
let new.options[opt] = stridx(options, opt) >= 0
......@@ -1376,10 +1376,10 @@ endfunction
" Log function when debugging.
function s:coq.log_debug (kind, head, ...)
if stridx(b:coq_debug, a:kind) < 0
if stridx(g:coq_debug, a:kind) < 0
return
endif
if stridx(b:coq_debug, 't') >= 0
if stridx(g:coq_debug, 't') >= 0
let s = strftime('[%H:%M:%S] ')
else
let s = ''
......
......@@ -197,8 +197,8 @@ will set the option 'Printing Implicit' as boolean to true.
=============================================================================
4. Configuration *coq-config*
Options for the Coq interaction plugin are read from the buffer variable
variable *b:coq_options* on startup. This variable is expected to be string,
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".
......@@ -235,8 +235,8 @@ The public Git repository of the project can be found at
*coq-debugging*
The Coq interaction plugin can be run in debugging mode by setting the
*b:coq_debug* variable. In this case, an extra window will be open on startup
and debugging messages will be appended there. The *b:coq_debug* variable is
*g:coq_debug* variable. In this case, an extra window will be open on startup
and debugging messages will be appended there. The *g:coq_debug* variable is
expected to be string, the presence of each letter below will trigger the
display of a particular kind of information:
......
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