Commit d3d57342 authored by Manu Beffara's avatar Manu Beffara
Browse files

Added a command :CoqQuery.

parent 256ddd31
......@@ -55,7 +55,8 @@ commands are provided:
- `:CoqQuit` ends the current interactive session,
- `:CoqNext` sends the next sentence to Coq,
- `:CoqRewind` rewinds by one sentence,
- `:CoqToCursor` sends or rewinds up to the current cursor position.
- `:CoqToCursor` sends or rewinds up to the current cursor position,
- `:CoqQuery {text}` sends a query in the current state.
Key mappings compatible with CoqIDE are installed by the `:CoqStart`
......@@ -935,6 +935,21 @@ function s:coq.return_init (return, d) abort
call a:return(a:d)
" query(text, state_id) {{{3
" -> {message}
" Perform a query in some state.
function s:coq.call_query (text, state_id, return, dict) abort
call self.log('r', "call", "Query", a:text, a:state_id)
\ ['pair', {},
\ ['string', {}, a:text],
\ ['state_id', {'val': a:state_id}]],
\ a:return, a:dict,
\ [[['string', {}, '*message']], {}])
" == Handling feedback == {{{2
......@@ -1344,6 +1359,21 @@ function s:coq.send_until_loop (d) abort
call self.show_goals()
" Send a query for the focussed state.
function s:coq.query (text) abort
call self.infos.clear()
call self.call_query(a:text, self.focus, self.query_return, {})
function s:coq.query_return (d) abort
if a:d.success
call self.infos.write(a:d.message)
call self.infos.write(s:richpp_format(a:d.message))
" == Commands and mappings == {{{2
......@@ -1353,6 +1383,7 @@ function! coqtop#Start () abort
command! -buffer CoqNext :call b:coq.send_next()
command! -buffer CoqRewind :call b:coq.rewind()
command! -buffer CoqToCursor :call b:coq.to_cursor()
command! -buffer -nargs=1 CoqQuery :call b:coq.query("<args>")
nnoremap <buffer> <silent> <C-Down> :CoqNext<CR>
nnoremap <buffer> <silent> <C-Up> :CoqRewind<CR>
......@@ -1377,6 +1408,7 @@ function! coqtop#Quit () abort
delcommand CoqNext
delcommand CoqRewind
delcommand CoqToCursor
delcommand CoqQuery
nunmap <buffer> <C-Down>
nunmap <buffer> <C-Right>
......@@ -112,6 +112,10 @@ are defined when starting a session and undefined when closing a session.
:CoqToCursor Check sentences or rewind, so that the last sentence before
the cursor is checked.
:CoqQuery {text}
Send the {text} as a query to Coq in the current state. The
{text} must be a complete sentence.
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