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
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
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 () ->
*)
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)
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
| `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
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
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 ()
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 =
projects / helm.git / blobdiff