diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2015-06-19 12:53:51 +0200 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-02 09:17:38 +0200 |
| commit | 6cc27d2ca57a5d2fedfa52d8b44c37c60ccb6988 (patch) | |
| tree | 4d30728dd551ccede5284e301feea86bf78d32d7 | |
| parent | cf5baeccf3cf7c24ccc69aa728bfe836fba5230a (diff) | |
Add a [Show Proof.] query to CoqIDE.
| -rw-r--r-- | ide/coqide.ml | 14 | ||||
| -rw-r--r-- | ide/coqide_ui.ml | 1 |
2 files changed, 13 insertions, 2 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 758a5a4c9..2d1ba72f3 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -677,18 +677,27 @@ let searchabout sn = let searchabout () = on_current_term searchabout +let doquery query sn = + sn.messages#clear; + Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore + +let showproof () = + let query = "Show Proof." in + on_current_term (doquery query) + let otherquery command sn = let word = get_current_word sn in if word <> "" then let query = command ^ " " ^ word ^ "." in - sn.messages#clear; - Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore + doquery query sn let otherquery command = cb_on_current_term (otherquery command) let query command _ = if command = "Search" || command = "SearchAbout" then searchabout () + else if command = "Show Proof" + then showproof () else otherquery command () end @@ -1109,6 +1118,7 @@ let build_ui () = qitem "About" (Some "<Ctrl><Shift>A"); qitem "Locate" (Some "<Ctrl><Shift>L"); qitem "Print Assumptions" (Some "<Ctrl><Shift>N"); + qitem "Show Proof" (Some "<Ctrl><Shift>R"); ]; menu tools_menu [ diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index edfe28b26..65735240a 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -119,6 +119,7 @@ let init () = <menuitem action='About' /> <menuitem action='Locate' /> <menuitem action='Print Assumptions' /> + <menuitem action='Show Proof' /> </menu> <menu name='Tools' action='Tools'> <menuitem action='Comment' /> |