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
(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;
connect_menu_item main#saveMenuItem saveScript;
connect_menu_item main#saveAsMenuItem saveAsScript;
connect_menu_item main#newMenuItem newScript;
+ connect_menu_item main#showCoercionsGraphMenuItem
+ (fun _ ->
+ let c = MatitaMathView.cicBrowser () in
+ c#load (`About `Coercions));
+ connect_menu_item main#showAutoGuiMenuItem
+ (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status);
(* script monospace font stuff *)
self#updateFontSize ();
(* debug menu *)