X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=f032831cbe2687c4638319f598407affd3e79883;hb=111df95ac03f2ee21dfa2422a7f531f675b1c16d;hp=e2a5588dc178dc2f6eb00394c5658f2e9013f621;hpb=aa6bc1bdfadf705fb3f8cc55291deab63c9e875c;p=helm.git diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index e2a5588dc..f032831cb 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/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 @@ -234,16 +229,40 @@ class interpErrorModel = let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.source_buffer) notify_exn offset errorll = + assert (List.flatten errorll <> []); let errorll' = let remove_non_significant = List.filter (fun (_env,_diff,_loc,_msg,significant) -> significant) in if all_passes then errorll else let safe_list_nth l n = try List.nth l n with Failure _ -> [] in (* We remove passes 1,2 and 5,6 *) - []::[] - ::(remove_non_significant (safe_list_nth errorll 2)) - ::(remove_non_significant (safe_list_nth errorll 3)) - ::[]::[] + let res = + []::[] + ::(remove_non_significant (safe_list_nth errorll 2)) + ::(remove_non_significant (safe_list_nth errorll 3)) + ::[]::[] + in + if List.flatten res <> [] then res + else + (* all errors (if any) are not significant: we keep them *) + let res = + []::[] + ::(safe_list_nth errorll 2) + ::(safe_list_nth errorll 3) + ::[]::[] + in + if List.flatten res <> [] then + begin + HLog.warn + "All disambiguation errors are not significant. Showing them anyway." ; + res + end + else + begin + HLog.warn + "No errors in phases 2 and 3. Showing all errors in all phases" ; + errorll + end in let choices = let pass = ref 0 in @@ -754,7 +773,11 @@ 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; @@ -945,8 +968,8 @@ 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 ~term_pp:CicNotationPp.pp_term + ~lazy_term_pp:CicNotationPp.pp_term ast) () in let tac_w_term ast _ = @@ -958,13 +981,14 @@ class gui () = ~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)); @@ -975,7 +999,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; @@ -984,12 +1008,27 @@ 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 ~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 -> + 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 *) HLog.set_log_callback self#console#log_callback; GtkSignal.user_handler :=