reductions_menu_item#set_submenu reductions;
tactics_menu_item#set_submenu tactics;
let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in
reductions_menu_item#set_submenu reductions;
tactics_menu_item#set_submenu tactics;
let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () 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)
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)
(MatitaScript.current ())#advance ~statement () in
connect_menu_item copy gui#copy;
connect_menu_item normalize (reduction_action `Normalize);
(MatitaScript.current ())#advance ~statement () in
connect_menu_item copy gui#copy;
connect_menu_item normalize (reduction_action `Normalize);
connect_menu_item simplify (reduction_action `Simpl);
connect_menu_item whd (reduction_action `Whd);
menu#popup ~button:right_button ~time
connect_menu_item simplify (reduction_action `Simpl);
connect_menu_item whd (reduction_action `Whd);
menu#popup ~button:right_button ~time
let add_tab markup goal_switch =
let goal = Stack.goal_of_switch goal_switch in
if not (List.mem goal !added_goals) then begin
let add_tab markup goal_switch =
let goal = Stack.goal_of_switch goal_switch in
if not (List.mem goal !added_goals) then begin
page2goal <- (!page, goal_switch) :: page2goal;
goal2page <- (goal_switch, !page) :: goal2page;
incr page;
page2goal <- (!page, goal_switch) :: page2goal;
goal2page <- (goal_switch, !page) :: goal2page;
incr page;
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;
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;
match self#currentCicUri with
| Some uri -> self#load (`Metadata (`Deps (`Back, uri)))
| None -> ());
match self#currentCicUri with
| Some uri -> self#load (`Metadata (`Deps (`Back, uri)))
| None -> ());
| `About `Coercions -> self#coerchgraph true ()
| `Check term -> self#_loadCheck term
| `Cic (term, metasenv) -> self#_loadTermCic term metasenv
| `About `Coercions -> self#coerchgraph true ()
| `Check term -> self#_loadCheck term
| `Cic (term, metasenv) -> self#_loadTermCic term metasenv
| `Dir dir -> self#_loadDir dir
| `HBugs `Tutors -> self#_loadHBugsTutors
| `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) ->
| `Dir dir -> self#_loadDir dir
| `HBugs `Tutors -> self#_loadHBugsTutors
| `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) ->
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
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