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)
+ | None -> ());
(* fill dep graph contextual menu *)
let go_menu_item =
val model =
new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
+ val model_univs =
+ new MatitaGtkMisc.multiStringListModel ~cols:2 win#universesTreeview
val mutable lastDir = "" (* last loaded "directory" *)
*)
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
| `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) ->
self#dependencies dir uri ()
| `Uri uri -> self#_loadUriManagerUri uri
+ | `Univs uri -> self#_loadUnivs uri
| `Whelp (query, results) ->
set_whelp_query query;
self#_loadList (List.map (fun r -> "obj",
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
| 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 ()
let uri = UriManager.strip_xpointer uri in
let (obj, _) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
self#_loadObj obj
+
+ method private _loadUnivs uri =
+ let uri = UriManager.strip_xpointer uri in
+ let (_, u) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let _,us = CicUniv.do_rank u in
+ let l =
+ List.map
+ (fun u ->
+ [ CicUniv.string_of_universe u ; string_of_int (CicUniv.get_rank u)])
+ us
+ in
+ self#_loadList2 l
method private _loadDir dir =
let content = Http_getter.ls ~local:false dir in
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 =
model#list_store#clear ();
List.iter (fun (tag, s) -> model#easy_append ~tag s) l;
self#_showList
+
+ method private _loadList2 l =
+ model_univs#list_store#clear ();
+ List.iter model_univs#easy_mappend l;
+ self#_showList2
(** { public methods, all must call _load!! } *)