From 6cc27d2ca57a5d2fedfa52d8b44c37c60ccb6988 Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Fri, 19 Jun 2015 12:53:51 +0200
Subject: Add a [Show Proof.] query to CoqIDE.

---
 ide/coqide.ml    | 14 ++++++++++++--
 ide/coqide_ui.ml |  1 +
 2 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 758a5a4c99..2d1ba72f3b 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 edfe28b261..65735240aa 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' />
-- 
cgit v1.2.3