...

[helm.git] / helm / software / matita / matitaMathView.ml

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index d8c02af44df108cbc2afc2cc1cdf7a23177f85cf..e6c26179132205f9028779dc0a8d7868b9271f43 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -814,6 +814,29 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     win#queryInputText#set_text input;
     combo#set_active (aux 0 queries);
   in
+  let searchText = 
+    GSourceView.source_view ~auto_indent:false ~editable:false ()
+  in
+  let _ =
+     win#scrolledwinContent#add (searchText :> GObj.widget);
+     let callback () = 
+       let text = win#entrySearch#text in
+       let highlight start end_ =
+         searchText#source_buffer#move_mark `INSERT ~where:start;
+         searchText#source_buffer#move_mark `SEL_BOUND ~where:end_;
+         searchText#scroll_mark_onscreen `INSERT
+       in
+       let iter = searchText#source_buffer#get_iter `SEL_BOUND in
+       match iter#forward_search text with
+       | None -> 
+           (match searchText#source_buffer#start_iter#forward_search text with
+           | None -> ()
+           | Some (start,end_) -> highlight start end_)
+       | Some (start,end_) -> highlight start end_
+     in
+     ignore(win#entrySearch#connect#activate ~callback);
+     ignore(win#buttonSearch#connect#clicked ~callback);
+  in
   let set_whelp_query txt =
     let query, arg = 
       try
@@ -890,8 +913,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       win#mathOrListNotebook#set_show_tabs false;
       win#browserForwardButton#misc#set_sensitive false;
       win#browserBackButton#misc#set_sensitive false;
-      ignore (win#browserUri#entry#connect#activate (handle_error' (fun () ->
-        self#loadInput win#browserUri#entry#text)));
+      ignore (win#browserUri#connect#activate (handle_error' (fun () ->
+        self#loadInput win#browserUri#text)));
       ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () ->
         self#load (`About `Current_proof))));
       ignore (win#browserRefreshButton#connect#clicked
@@ -926,6 +949,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
         match self#currentCicUri with
         | Some uri -> self#load (`Metadata (`Deps (`Back, uri)))
         | None -> ());
+      connect_menu_item win#browserCloseMenuItem (fun () ->
+        let my_id = Oo.id self in
+        cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
+        win#toplevel#misc#hide(); win#toplevel#destroy ());
       (* remove hbugs *)
       (*
       connect_menu_item win#hBugsTutorsMenuItem (fun () ->
@@ -933,7 +960,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       *)
       win#hBugsTutorsMenuItem#misc#hide ();
       connect_menu_item win#browserUrlMenuItem (fun () ->
-        win#browserUri#entry#misc#grab_focus ());
+        win#browserUri#misc#grab_focus ());
       connect_menu_item win#univMenuItem (fun () ->
         match self#currentCicUri with
         | Some uri -> self#load (`Univs uri)
@@ -1018,6 +1045,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     method private _showMath = win#mathOrListNotebook#goto_page  0
     method private _showList = win#mathOrListNotebook#goto_page  1
     method private _showList2 = win#mathOrListNotebook#goto_page 5
+    method private _showSearch = win#mathOrListNotebook#goto_page 6
     method private _showGviz = win#mathOrListNotebook#goto_page  3
     method private _showHBugs = win#mathOrListNotebook#goto_page 4
 
@@ -1044,6 +1072,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           | `About `Us -> self#egg ()
           | `About `CoercionsFull -> self#coerchgraph false ()
           | `About `Coercions -> self#coerchgraph true ()
+          | `About `TeX -> self#tex ()
+          | `About `Grammar -> self#grammar () 
           | `Check term -> self#_loadCheck term
           | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
           | `Dir dir -> self#_loadDir dir
@@ -1096,6 +1126,29 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       load_coerchgraph tred ();
       self#_showGviz
 
+    method private tex () =
+      let text = String.concat "\n"
+        (List.map (fun (k,vs) -> 
+           let vs = 
+             List.sort (fun a b -> String.length a - String.length b) vs
+           in
+           let vs = 
+             if List.length vs < 4 then vs else 
+             let vs, _ = HExtlib.split_nth 4 vs in vs
+           in
+           k ^ "\t" ^ String.concat ", " vs)
+        (Utf8Macro.pp_table ())) 
+      in
+      self#_loadText text
+
+    method private _loadText text =
+      searchText#source_buffer#set_text text;
+      win#entrySearch#misc#grab_focus ();
+      self#_showSearch
+
+    method private grammar () =
+      self#_loadText (Print_grammar.ebnf_of_term ());
+
     method private home () =
       self#_showMath;
       match self#script#grafite_status.proof_status with
@@ -1146,7 +1199,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_showHBugs
 
     method private setEntry entry =
-      win#browserUri#entry#set_text (MatitaTypes.string_of_entry entry);
+      win#browserUri#set_text (MatitaTypes.string_of_entry entry);
       current_entry <- entry
 
     method private _loadObj obj =