- (* toolbar *)
- let module A = GrafiteAst in
- let hole = CicNotationPt.UserInput in
- let loc = HExtlib.dummy_floc in
- let tac ast _ =
- if (MatitaScript.current ())#onGoingProof () then
- (MatitaScript.current ())#advance
- ~statement:("\n"
- ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
- ~lazy_term_pp:CicNotationPp.pp_term ast)
- ()
- in
- let tac_w_term ast _ =
- if (MatitaScript.current ())#onGoingProof () then
- let buf = source_buffer in
- buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
- ("\n"
- ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
- ~lazy_term_pp:CicNotationPp.pp_term ast)
- in
- let tbar = main in
- connect_button tbar#introsButton (tac (A.Intros (loc, (None, []))));
- connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
- connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
- connect_button tbar#elimButton (tac_w_term
- (let pattern = None, [], Some CicNotationPt.UserInput in
- A.Elim (loc, hole, None, pattern, (None, []))));
- connect_button tbar#elimTypeButton (tac_w_term
- (A.ElimType (loc, hole, None, (None, []))));
- connect_button tbar#splitButton (tac (A.Split loc));
- connect_button tbar#leftButton (tac (A.Left loc));
- connect_button tbar#rightButton (tac (A.Right loc));
- connect_button tbar#existsButton (tac (A.Exists loc));
- connect_button tbar#reflexivityButton (tac (A.Reflexivity loc));
- connect_button tbar#symmetryButton (tac (A.Symmetry loc));
- connect_button tbar#transitivityButton
- (tac_w_term (A.Transitivity (loc, hole)));
- connect_button tbar#assumptionButton (tac (A.Assumption loc));
- connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
- connect_button tbar#autoButton (tac (A.AutoBatch (loc,[])));
- MatitaGtkMisc.toggle_widget_visibility
- ~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
- ~check:main#tacticsBarMenuItem;