X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaGui.ml;h=f849dc25f5b5e84d09e067dd759687da415a0918;hb=dfc523454502ccab6a154a32d1d9b4d941d9a6a0;hp=79962a35cd86169f625acd0bf2597a7afcf59d77;hpb=7fed865c7cd7ea742a360158a931a3fa734ee446;p=helm.git diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index 79962a35c..f849dc25f 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 @@ -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 @@ -301,8 +320,31 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView. uniq ((o1,res) :: tl) | h1::tl -> h1 :: uniq tl in - List.map (fun o,l -> o,List.sort choices_compare_by_passes l) - (uniq (List.stable_sort choices_compare choices)) + (* Errors in phase 3 that are not also in phase 4 are filtered out *) + let filter_phase_3 choices = + if all_passes then choices + else + let filter = + HExtlib.filter_map + (function + (loffset,messages) -> + let filtered_messages = + HExtlib.filter_map + (function + [3],_,_,_ -> None + | item -> Some item + ) messages + in + if filtered_messages = [] then + None + else + Some (loffset,filtered_messages)) + in + filter choices + in + filter_phase_3 + (List.map (fun o,l -> o,List.sort choices_compare_by_passes l) + (uniq (List.stable_sort choices_compare choices))) in match choices with [] -> assert false @@ -731,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 @@ -843,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 @@ -914,59 +964,32 @@ class gui () = ignore (adj#connect#changed (fun _ -> adj#set_value (adj#upper -. adj#page_size))); console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version); - (* toolbar *) - let module A = GrafiteAst in - let hole = CicNotationPt.UserInput in - let loc = HExtlib.dummy_floc in - let tac ast _ = - 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))) - () - in - let tac_w_term ast _ = - if (MatitaScript.current ())#onGoingProof () then - let buf = source_buffer in - buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) - ("\n" - ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term - ~lazy_term_pp:CicNotationPp.pp_term ast) - in - let tbar = main in - 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, []))); - connect_button tbar#elimTypeButton (tac_w_term - (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)); - connect_button tbar#existsButton (tac (A.Exists loc)); - connect_button tbar#reflexivityButton (tac (A.Reflexivity loc)); - connect_button tbar#symmetryButton (tac (A.Symmetry loc)); - connect_button tbar#transitivityButton - (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,[]))); - MatitaGtkMisc.toggle_widget_visibility - ~widget:(main#tacticsButtonsHandlebox :> GObj.widget) - ~check:main#tacticsBarMenuItem; + (* TO BE REMOVED *) + main#tacticsButtonsHandlebox#misc#hide (); + main#tacticsBarMenuItem#misc#hide (); + main#scriptNotebook#remove_page 1; + main#scriptNotebook#set_show_tabs false; + (* / TO BE REMOVED *) let module Hr = Helm_registry in - if - 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); + 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 := @@ -1111,6 +1134,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 *) @@ -1350,11 +1379,13 @@ class gui () = end method setStar name b = - let l = main#scriptLabel in + let w = main#toplevel in + let set x = w#set_title x in + let name = "Matita - " ^ name in if b then - l#set_text (name ^ " *") + set (name ^ " *") else - l#set_text (name) + set (name) method private _enableSaveTo file = script_fname <- Some file; @@ -1653,18 +1684,16 @@ let interactive_string_choice | Some uris -> uris) let interactive_interp_choice () text prefix_len choices = -(* List.iter (fun (l,_,_) -> - List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in - Printf.eprintf "(%d,%d)" start stop) l; prerr_endline "") - ((List.hd choices)); *) +(*List.iter (fun l -> prerr_endline "==="; List.iter (fun (_,id,dsc) -> prerr_endline (id ^ " = " ^ dsc)) l) choices;*) let filter_choices filter = let rec is_compatible filter = function [] -> true - | (_,id,dsc)::tl -> + | ([],_,_)::tl -> is_compatible filter tl + | (loc::tlloc,id,dsc)::tl -> try - if List.assoc id filter = dsc then - is_compatible filter tl + if List.assoc (loc,id) filter = dsc then + is_compatible filter ((tlloc,id,dsc)::tl) else false with @@ -1672,12 +1701,14 @@ let interactive_interp_choice () text prefix_len choices = in List.filter (fun (_,interp) -> is_compatible filter interp) in - let rec get_choices id = + let rec get_choices loc id = function [] -> [] | (_,he)::tl -> - let _,_,dsc = List.find (fun (_,id',_) -> id = id') he in - dsc :: (List.filter (fun dsc' -> dsc <> dsc') (get_choices id tl)) + let _,_,dsc = + List.find (fun (locs,id',_) -> id = id' && List.mem loc locs) he + in + dsc :: (List.filter (fun dsc' -> dsc <> dsc') (get_choices loc id tl)) in let example_interp = match choices with @@ -1692,19 +1723,22 @@ let interactive_interp_choice () text prefix_len choices = let rec classify ids filter partial_interpretations = match ids with [] -> List.map fst partial_interpretations - | (locs,id,_)::tl -> - let choices = get_choices id partial_interpretations in + | ([],_,_)::tl -> classify tl filter partial_interpretations + | (loc::tlloc,id,dsc)::tl -> + let choices = get_choices loc id partial_interpretations in let chosen_dsc = match choices with - [dsc] -> dsc + [] -> prerr_endline ("NO CHOICES FOR " ^ id); assert false + | [dsc] -> dsc | _ -> - match ask_user id locs choices with + match ask_user id [loc] choices with [x] -> x | _ -> assert false in - let filter = (id,chosen_dsc)::filter in - let compatible_interps = filter_choices filter partial_interpretations in - classify tl filter compatible_interps in + let filter = ((loc,id),chosen_dsc)::filter in + let compatible_interps = filter_choices filter partial_interpretations in + classify ((tlloc,id,dsc)::tl) filter compatible_interps + in let enumerated_choices = let idx = ref ~-1 in List.map (fun interp -> incr idx; !idx,interp) choices