LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri
~writable:true in
let save () =
- let metadata_fname =
- LibraryMisc.metadata_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:true in
let lexicon_fname =
LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~baseuri ~writable:true
in
GrafiteMarshal.save_moo moo_fname
grafite_status.GrafiteTypes.moo_content_rev;
- LibraryNoDb.save_metadata metadata_fname
- lexicon_status.LexiconEngine.metadata;
LexiconMarshal.save_lexicon lexicon_fname
lexicon_status.LexiconEngine.lexicon_content_rev
in
if (MatitaScript.current ())#onGoingProof () then
(MatitaScript.current ())#advance
~statement:("\n"
- ^ GrafiteAstPp.pp_tactical ~term_pp:CicNotationPp.pp_term
- ~lazy_term_pp:CicNotationPp.pp_term (A.Tactic (loc, ast)))
+ ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
+ ~lazy_term_pp:CicNotationPp.pp_term ast)
()
in
let tac_w_term ast _ =
~lazy_term_pp:CicNotationPp.pp_term ast)
in
let tbar = main in
- connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
+ 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, [])));
+ A.Elim (loc, hole, None, pattern, (None, []))));
connect_button tbar#elimTypeButton (tac_w_term
- (A.ElimType (loc, hole, None, None, [])));
+ (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));
(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.Auto (loc,[])));
+ connect_button tbar#autoButton (tac (A.AutoBatch (loc,[])));
MatitaGtkMisc.toggle_widget_visibility
~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
~check:main#tacticsBarMenuItem;