X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=7cb2aa7cbec948ef3cdfbad183f8e959eedd0fb8;hb=b7aefa8f362d07bf9042f6879252345e69da07c8;hp=d8c02af44df108cbc2afc2cc1cdf7a23177f85cf;hpb=c2957e84a0fa8fe60bbbe89f4923a50bd626444d;p=helm.git diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index d8c02af44..7cb2aa7cb 100644 --- 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 @@ -1072,15 +1102,21 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) Lazy.force load_easter_egg method private redraw_gviz ?center_on () = - let tmpfile, oc = Filename.open_temp_file "matita" ".dot" in - let fmt = Format.formatter_of_out_channel oc in - MetadataDeps.DepGraph.render fmt gviz_graph; - close_out oc; - gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile; - (match center_on with - | None -> () - | Some uri -> gviz#center_on_href (UriManager.string_of_uri uri)); - HExtlib.safe_remove tmpfile + if Sys.command "which dot" = 0 then + let tmpfile, oc = Filename.open_temp_file "matita" ".dot" in + let fmt = Format.formatter_of_out_channel oc in + MetadataDeps.DepGraph.render fmt gviz_graph; + close_out oc; + gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile; + (match center_on with + | None -> () + | Some uri -> gviz#center_on_href (UriManager.string_of_uri uri)); + HExtlib.safe_remove tmpfile + else + MatitaGtkMisc.report_error ~title:"graphviz error" + ~message:("Graphviz is not installed but is necessary to render "^ + "the graph of dependencies amoung objects. Please install it.") + ~parent:win#toplevel () method private dependencies direction uri () = let dbd = LibraryDb.instance () in @@ -1096,16 +1132,55 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) load_coerchgraph tred (); self#_showGviz + method private tex () = + let b = Buffer.create 1000 in + Printf.bprintf b "UTF-8 equivalence classes (rotate with ALT-L):\n\n"; + List.iter + (fun l -> + List.iter (fun sym -> + Printf.bprintf b " %s" (Glib.Utf8.from_unichar sym) + ) l; + Printf.bprintf b "\n"; + ) + (List.sort + (fun l1 l2 -> compare (List.hd l1) (List.hd l2)) + (Virtuals.get_all_eqclass ())); + Printf.bprintf b "\n\nVirtual keys (trigger with ALT-L):\n\n"; + List.iter + (fun tag, items -> + Printf.bprintf b " %s:\n" tag; + List.iter + (fun names, symbol -> + Printf.bprintf b " \t%s\t%s\n" + (Glib.Utf8.from_unichar symbol) + (String.concat ", " names)) + (List.sort + (fun (_,a) (_,b) -> compare a b) + items); + Printf.bprintf b "\n") + (List.sort + (fun (a,_) (b,_) -> compare a b) + (Virtuals.get_all_virtuals ())); + self#_loadText (Buffer.contents b) + + 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 | Proof (uri, metasenv, _subst, bo, ty, attrs) -> let name = UriManager.name_of_uri (HExtlib.unopt uri) in - let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in + let obj = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in self#_loadObj obj | Incomplete_proof { proof = (uri, metasenv, _subst, bo, ty, attrs) } -> let name = UriManager.name_of_uri (HExtlib.unopt uri) in - let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in + let obj = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in self#_loadObj obj | _ -> self#blank () @@ -1146,7 +1221,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 =