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
notify_exn exc;
unlock_world ()
in
- worker_thread := Some (Thread.create thread_main ()) in
+ (*thread_main ();*)
+ worker_thread := Some (Thread.create thread_main ())
+ in
let kill_worker =
(* the following lines are from Xavier Leroy: http://alan.petitepomme.net/cwn/2005.11.08.html *)
let interrupt = ref None in
| None -> true
| Some path ->
let is_prefix_of d1 d2 =
+ let d1 = MatitamakeLib.normalize_path d1 in
+ let d2 = MatitamakeLib.normalize_path d2 in
let len1 = String.length d1 in
let len2 = String.length d2 in
if len2 < len1 then
if (MatitaScript.current ())#onGoingProof () then
(MatitaScript.current ())#advance
~statement:("\n"
- ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
+ ^ GrafiteAstPp.pp_tactic
+ ~map_unicode_to_tex:(Helm_registry.get_bool
+ "matita.paste_unicode_as_tex")
+ ~term_pp:CicNotationPp.pp_term
~lazy_term_pp:CicNotationPp.pp_term ast)
()
in
buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
("\n"
^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
+ ~map_unicode_to_tex:(Helm_registry.get_bool
+ "matita.paste_unicode_as_tex")
~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;
MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem
~callback:(fun enabled ->
Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled);
- if not (Helm_registry.has "matita.paste_unicode_as_tex") then
- Helm_registry.set_bool "matita.paste_unicode_as_tex" true;
main#unicodeAsTexMenuItem#set_active
(Helm_registry.get_bool "matita.paste_unicode_as_tex");
(* log *)
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 *)