reductions_menu_item#set_submenu reductions;
tactics_menu_item#set_submenu tactics;
let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in
- let reduce = add_menu_item ~menu:reductions ~label:"Reduce" () in
let simplify = add_menu_item ~menu:reductions ~label:"Simplify" () in
let whd = add_menu_item ~menu:reductions ~label:"Weak head" () in
menu#append (GMenu.separator_item ());
let copy = add_menu_item ~stock:`COPY () in
let gui = get_gui () in
List.iter (fun item -> item#misc#set_sensitive gui#canCopy)
- [ copy; check; normalize; reduce; simplify; whd ];
+ [ copy; check; normalize; simplify; whd ];
let reduction_action kind () =
let pat = self#tactic_text_pattern_of_selection in
let statement =
(MatitaScript.current ())#advance ~statement () in
connect_menu_item copy gui#copy;
connect_menu_item normalize (reduction_action `Normalize);
- connect_menu_item reduce (reduction_action `Reduce);
connect_menu_item simplify (reduction_action `Simpl);
connect_menu_item whd (reduction_action `Whd);
menu#popup ~button:right_button ~time
method load_logo =
notebook#set_show_tabs false;
- notebook#append_page logo
+ ignore(notebook#append_page logo)
method load_logo_with_qed =
notebook#set_show_tabs false;
- notebook#append_page logo_with_qed
+ ignore(notebook#append_page logo_with_qed)
method reset =
cicMathView#remove_selections;
let add_tab markup goal_switch =
let goal = Stack.goal_of_switch goal_switch in
if not (List.mem goal !added_goals) then begin
- notebook#append_page ~tab_label:(tab_label markup) (win goal_switch);
+ ignore(notebook#append_page
+ ~tab_label:(tab_label markup) (win goal_switch));
page2goal <- (!page, goal_switch) :: page2goal;
goal2page <- (goal_switch, !page) :: goal2page;
incr page;
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
ignore (win#toplevel#event#connect#delete (fun _ ->
let my_id = Oo.id self in
cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
- if !cicBrowsers = [] &&
- Helm_registry.get "matita.mode" = "cicbrowser"
- then
- GMain.quit ();
false));
ignore(win#whelpResultTreeview#connect#row_activated
~callback:(fun _ _ ->
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 () ->
self#load (`HBugs `Tutors));
+ *)
+ 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
- | `Development d -> self#_showDevelDeps d
| `Dir dir -> self#_loadDir dir
| `HBugs `Tutors -> self#_loadHBugsTutors
| `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",
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
+ | Some uri -> gviz#center_on_href (UriManager.string_of_uri uri))
+(* HExtlib.safe_remove tmpfile *)
method private dependencies direction uri () =
let dbd = LibraryDb.instance () in
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 _showDevelDeps d =
- match MatitamakeLib.development_for_name d with
- | None -> ()
- | Some devel ->
- (match MatitamakeLib.dot_for_development devel with
- | None -> ()
- | Some fname ->
- gviz#load_graph_from_file ~gviz_cmd:"tred | dot" fname;
- self#_showGviz)
-
method private _loadObj obj =
(* showMath must be done _before_ loading the document, since if the
* widget is not mapped (hidden by the notebook) the document is not
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!! } *)
projects / helm.git / blobdiff