Nice output of SearchAbout command in CoqIDE

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15779 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 107 insertions, 15 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 844086fe1..b6c6030e3 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1735,6 +1735,28 @@ let main files =
   let tactic_shortcut s sc = GAction.add_action s ~label:("_"^s)
     ~accel:(current.modifier_for_tactics^sc)
     ~callback:(fun _ -> do_if_active (fun handle a -> a#tactic_wizard handle [s]) ()) in
+  let query_searchabout () =
+    let word = get_current_word () in
+    let term = session_notebook#current_term in
+    let query handle =
+      let results = Coq.search handle [Interface.SubType_Pattern word, true] in
+      let results = match results with | Interface.Good l -> l | _ -> [] in
+      let buf =  term.message_view#buffer in
+      let insert result =
+        let basename = result.Interface.search_answer_base_name in
+        let path = result.Interface.search_answer_full_path in
+        let name = String.concat "." path ^ "." ^ basename in
+        let tpe = result.Interface.search_answer_type in
+        buf#insert ~tags:[Tags.Message.item] name;
+        buf#insert "\n";
+        buf#insert tpe;
+        buf#insert "\n";
+      in
+      term.message_view#clear ();
+      List.iter insert results
+    in
+    Coq.try_grab term.toplvl query ignore
+  in
   let query_callback command _ =
     let word = get_current_word () in
     let term = session_notebook#current_term in
@@ -1745,6 +1767,9 @@ let main files =
       try Coq.try_grab term.toplvl (f query) ignore
       with e -> term.message_view#push Interface.Error (Printexc.to_string e)
   in
+  let query_callback command _ =
+    if command = "SearchAbout" then query_searchabout () else query_callback command ()
+  in
   let query_shortcut s accel =
     GAction.add_action s ~label:("_"^s) ?accel ~callback:(query_callback s)
   in
@@ -1805,13 +1830,13 @@ let main files =
       GAction.add_action "Paste"
         ~callback:(fun _ -> emit_to_focus GtkText.View.S.paste_clipboard) ~stock:`PASTE;
       GAction.add_action "Find" ~stock:`FIND
-        ~callback:(fun _ -> session_notebook#current_term.finder#show_find ());
+        ~callback:(fun _ -> session_notebook#current_term.finder#show `FIND);
       GAction.add_action "Find Next" ~label:"Find _Next" ~stock:`GO_DOWN ~accel:"F3"
         ~callback:(fun _ -> session_notebook#current_term.finder#find_forward ());
       GAction.add_action "Find Previous" ~label:"Find _Previous" ~stock:`GO_UP ~accel:"<Shift>F3"
         ~callback:(fun _ -> session_notebook#current_term.finder#find_backward ());
       GAction.add_action "Replace" ~stock:`FIND_AND_REPLACE
-        ~callback:(fun _ -> session_notebook#current_term.finder#show_replace ());
+        ~callback:(fun _ -> session_notebook#current_term.finder#show `REPLACE);
      GAction.add_action "Close Find" ~accel:"Escape"
         ~callback:(fun _ -> session_notebook#current_term.finder#hide ());
       GAction.add_action "Complete Word" ~label:"Complete Word" ~callback:(fun _ ->
diff --git a/ide/ide.mllib b/ide/ide.mllib
index d2f2f12fe..1c3b7f21e 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -10,7 +10,6 @@ Editable_cells
 Config_parser
 Tags
 Wg_Notebook
-Wg_Find
 Config_lexer
 Utf8_convert
 Preferences
@@ -20,6 +19,7 @@ Coq
 Gtk_parsing
 Wg_ProofView
 Wg_MessageView
+Wg_Find
 Wg_ScriptView
 Coq_lex
 Coq_commands
diff --git a/ide/tags.ml b/ide/tags.ml
index fe4db5705..cde831513 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -38,6 +38,7 @@ module Message =
 struct
   let table = GText.tag_table ()
   let error = make_tag table ~name:"error" [`FOREGROUND "red"]
+  let item = make_tag table ~name:"item" [`WEIGHT `BOLD]
 end
 
 let string_of_color clr =
diff --git a/ide/tags.mli b/ide/tags.mli
index a019b45db..a96ae98b9 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -30,6 +30,7 @@ module Message :
 sig
   val table : GText.tag_table
   val error : GText.tag
+  val item : GText.tag
 end
 
 val string_of_color : Gdk.color -> string
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index 8b5acce7b..21369d6f6 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-type mode =
-| Find
-| Replace
+type mode = [ `FIND | `REPLACE ]
 
 class finder (view : GText.view) =
 
@@ -92,7 +90,7 @@ class finder (view : GText.view) =
 
   object (self)
     val mutable last_found = None
-    val mutable mode = Find
+    val mutable mode : mode = `FIND
 
     method coerce = widget#coerce
 
@@ -172,15 +170,19 @@ class finder (view : GText.view) =
       self#find_from true starti self#search_text
 
     method private search_text = match mode with
-    | Find -> find_entry#text
-    | Replace -> r_find_entry#text
+    | `FIND -> find_entry#text
+    | `REPLACE -> r_find_entry#text
 
     method hide () =
       widget#misc#hide ();
       view#coerce#misc#grab_focus ()
 
-    method show_find () =
-      mode <- Find;
+    method show (mode : mode) = match mode with
+    | `FIND -> self#show_find ()
+    | `REPLACE -> self#show_replace ()
+
+    method private show_find () =
+      mode <- `FIND;
       let search =
         if self#coerce#misc#visible then
           r_find_entry#text
@@ -194,8 +196,8 @@ class finder (view : GText.view) =
       replace_box#misc#hide ();
       find_entry#misc#grab_focus ()
 
-    method show_replace () =
-      mode <- Replace;
+    method private show_replace () =
+      mode <- `REPLACE;
       let search =
         if self#coerce#misc#visible then
           find_entry#text
@@ -220,3 +222,61 @@ class finder (view : GText.view) =
       ()
 
   end
+
+class info (coqtop : Coq.coqtop) (view : GText.view) (msg_view : Wg_MessageView.message_view) =
+
+  let widget = GPack.vbox () in
+  (* SearchAbout part *)
+  let query_box = GPack.hbox ~packing:widget#add () in
+  let _ =
+    GMisc.label ~text:"SearchAbout:"
+      ~xalign:1.0
+      ~packing:query_box#pack ()
+  in
+  let find_entry = GEdit.entry
+    ~editable:true
+    ~packing:(query_box#pack ~expand:true)
+    ()
+  in
+  let next_button =
+    GButton.button
+      ~label:"_Go"
+      ~use_mnemonic:true
+(*       ~stock:`GO_DOWN *)
+      ~packing:query_box#pack
+      ()
+  in
+
+
+  object (self)
+    method coerce = widget#coerce
+
+    method private get_selected_word () =
+      let start = view#buffer#get_iter `INSERT in
+      let stop = view#buffer#get_iter `SEL_BOUND in
+      view#buffer#get_text ~start ~stop ()
+
+    method hide () =
+      widget#misc#hide ();
+      view#coerce#misc#grab_focus ()
+
+    method show () =
+      let search =
+        if self#coerce#misc#visible then find_entry#text
+        else
+          self#get_selected_word ()
+      in
+      find_entry#set_text search;
+      widget#misc#show ()
+
+    method private search () =
+      let search = find_entry#text in
+      let len = String.length search in
+      ()
+
+    initializer
+      let _ = self#hide () in
+      let _ = next_button#connect#clicked self#search in
+      ()
+
+  end
diff --git a/ide/wg_Find.mli b/ide/wg_Find.mli
index b0a421317..5337dae7c 100644
--- a/ide/wg_Find.mli
+++ b/ide/wg_Find.mli
@@ -6,12 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+type mode = [ `FIND | `REPLACE ]
+
 class finder : GText.view ->
   object
     method coerce : GObj.widget
     method hide : unit -> unit
-    method show_find : unit -> unit
-    method show_replace : unit -> unit
+    method show : mode -> unit
     method replace : unit -> unit
     method replace_all : unit -> unit
     method find_backward : unit -> unit
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index d4f353e50..bd6d517dc 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -11,6 +11,7 @@ class type message_view =
     inherit GObj.widget
     method clear : unit -> unit
     method push : Interface.message_level -> string -> unit
+    method buffer : GText.buffer
   end
 
 let message_view () : message_view =
@@ -35,4 +36,6 @@ let message_view () : message_view =
       buffer#insert ~tags msg;
       buffer#insert ~tags "\n"
 
+    method buffer = buffer
+
   end
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index 991b98163..f27f99afa 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -11,6 +11,7 @@ class type message_view =
     inherit GObj.widget
     method clear : unit -> unit
     method push : Interface.message_level -> string -> unit
+    method buffer : GText.buffer
   end
 
 val message_view : unit -> message_view