X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaGui.ml;h=fde6ba1ae2d9abde9b6a2b13bd6cfab1217d8065;hb=b2abc81f0b76224f6f4f526feaf1fefd6178ae7d;hp=b8d20cf3cace3c3557b2c872fe72af18c8ca2e9f;hpb=8a1b43d009dc6eb9a64e35e08fccbef4313140b8;p=helm.git diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index b8d20cf3c..fde6ba1ae 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -84,17 +84,12 @@ let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status = 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 @@ -778,13 +773,19 @@ class gui () = unlock_world () with | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> - interactive_error_interp source_buffer notify_exn offset errorll ; + (try + interactive_error_interp source_buffer notify_exn offset + errorll + with + exc -> notify_exn exc); unlock_world () | exc -> 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 @@ -890,6 +891,8 @@ class gui () = | 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 @@ -969,8 +972,11 @@ class gui () = 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 + ~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 let tac_w_term ast _ = @@ -979,16 +985,19 @@ class gui () = 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 - (A.Elim (loc, hole, None, None, []))); + (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, []))); + (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)); @@ -999,7 +1008,7 @@ class gui () = (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; @@ -1008,16 +1017,25 @@ class gui () = not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar") then main#tacticsBarMenuItem#set_active false; - MatitaGtkMisc.toggle_callback + MatitaGtkMisc.toggle_callback ~check:main#fullscreenMenuItem ~callback:(function | true -> main#toplevel#fullscreen () - | false -> main#toplevel#unfullscreen ()) - ~check:main#fullscreenMenuItem; + | false -> main#toplevel#unfullscreen ()); main#fullscreenMenuItem#set_active false; - MatitaGtkMisc.toggle_callback + MatitaGtkMisc.toggle_callback ~check:main#ppNotationMenuItem + ~callback:(function + | true -> + CicNotation.set_active_notations + (List.map fst (CicNotation.get_all_notations ())) + | false -> + CicNotation.set_active_notations []); + MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem + ~callback:(fun enabled -> Acic2content.hide_coercions := enabled); + MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem ~callback:(fun enabled -> - CicMetaSubst.use_low_level_ppterm_in_context := not enabled) - ~check:main#formulaePpMenuItem; + Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled); + main#unicodeAsTexMenuItem#set_active + (Helm_registry.get_bool "matita.paste_unicode_as_tex"); (* log *) HLog.set_log_callback self#console#log_callback; GtkSignal.user_handler := @@ -1162,6 +1180,12 @@ class gui () = 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 *)