X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaGui.ml;h=fde6ba1ae2d9abde9b6a2b13bd6cfab1217d8065;hb=b2abc81f0b76224f6f4f526feaf1fefd6178ae7d;hp=cf1c0de4df94a203ac73c6ea0ab04be63e8c0642;hpb=fae6f153d6dad76b6ccfce17a6b3d997db338d2e;p=helm.git diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index cf1c0de4d..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 @@ -133,35 +128,98 @@ class interpErrorModel = let cols = new GTree.column_list in let id_col = cols#add Gobject.Data.string in let dsc_col = cols#add Gobject.Data.string in - let interp_no_col = cols#add Gobject.Data.int in + let interp_no_col = cols#add Gobject.Data.caml in let tree_store = GTree.tree_store cols in let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in let id_view_col = GTree.view_column ~renderer:id_renderer () in let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in - fun tree_view choices -> + fun (tree_view: GTree.view) choices -> object initializer tree_view#set_model (Some (tree_store :> GTree.model)); ignore (tree_view#append_column id_view_col); ignore (tree_view#append_column dsc_view_col); tree_store#clear (); - let idx = ref ~-1 in + let idx1 = ref ~-1 in List.iter - (fun passes,env,_,_,_ -> - incr idx; - let interp_row = tree_store#append () in - tree_store#set ~row:interp_row ~column:id_col - ("Passes " ^ String.concat " " (List.map string_of_int passes)); - tree_store#set ~row:interp_row ~column:interp_no_col !idx; - List.iter - (fun (_, id, dsc) -> - let row = tree_store#append ~parent:interp_row () in - tree_store#set ~row ~column:id_col id; - tree_store#set ~row ~column:dsc_col dsc; - tree_store#set ~row ~column:interp_no_col !idx) - env) - choices + (fun _,lll -> + incr idx1; + let loc_row = + if List.length choices = 1 then + None + else + (let loc_row = tree_store#append () in + begin + match lll with + [passes,envs_and_diffs,_,_] -> + tree_store#set ~row:loc_row ~column:id_col + ("Error location " ^ string_of_int (!idx1+1) ^ + ", error message " ^ string_of_int (!idx1+1) ^ ".1" ^ + " (in passes " ^ + String.concat " " (List.map string_of_int passes) ^ + ")"); + tree_store#set ~row:loc_row ~column:interp_no_col + (!idx1,Some 0,None); + | _ -> + tree_store#set ~row:loc_row ~column:id_col + ("Error location " ^ string_of_int (!idx1+1)); + tree_store#set ~row:loc_row ~column:interp_no_col + (!idx1,None,None); + end ; + Some loc_row) in + let idx2 = ref ~-1 in + List.iter + (fun passes,envs_and_diffs,_,_ -> + incr idx2; + let msg_row = + if List.length lll = 1 then + loc_row + else + let msg_row = tree_store#append ?parent:loc_row () in + (tree_store#set ~row:msg_row ~column:id_col + ("Error message " ^ string_of_int (!idx1+1) ^ "." ^ + string_of_int (!idx2+1) ^ + " (in passes " ^ + String.concat " " (List.map string_of_int passes) ^ + ")"); + tree_store#set ~row:msg_row ~column:interp_no_col + (!idx1,Some !idx2,None); + Some msg_row) in + let idx3 = ref ~-1 in + List.iter + (fun (passes,env,_) -> + incr idx3; + let interp_row = + match envs_and_diffs with + _::_::_ -> + let interp_row = tree_store#append ?parent:msg_row () in + tree_store#set ~row:interp_row ~column:id_col + ("Interpretation " ^ string_of_int (!idx3+1) ^ + " (in passes " ^ + String.concat " " (List.map string_of_int passes) ^ + ")"); + tree_store#set ~row:interp_row ~column:interp_no_col + (!idx1,Some !idx2,Some !idx3); + Some interp_row + | [_] -> msg_row + | [] -> assert false + in + List.iter + (fun (_, id, dsc) -> + let row = tree_store#append ?parent:interp_row () in + tree_store#set ~row ~column:id_col id; + tree_store#set ~row ~column:dsc_col dsc; + tree_store#set ~row ~column:interp_no_col + (!idx1,Some !idx2,Some !idx3) + ) env + ) envs_and_diffs + ) lll ; + if List.length lll > 1 then + HExtlib.iter_option + (fun p -> tree_view#expand_row (tree_store#get_path p)) + loc_row + ) choices method get_interp_no tree_path = let iter = tree_store#get_iter tree_path in @@ -169,11 +227,43 @@ class interpErrorModel = end -let rec interactive_error_interp ?(all_passes=false) source_buffer notify_exn - offset errorll +let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.source_buffer) notify_exn offset errorll = + assert (List.flatten errorll <> []); let errorll' = - if all_passes then errorll else List.rev (List.tl (List.tl (List.rev errorll))) in + 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 *) + 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 List.flatten @@ -181,34 +271,88 @@ let rec interactive_error_interp ?(all_passes=false) source_buffer notify_exn (fun l -> incr pass; List.map - (fun (env,diff,offset,msg) -> [!pass], env, diff, offset, msg) l + (fun (env,diff,offset,msg,significant) -> + offset, [[!pass], [[!pass], env, diff], msg, significant]) l ) errorll') in (* Here we are doing a stable sort and list_uniq returns the latter "equal" element. I.e. we are showing the error corresponding to the most advanced disambiguation pass *) let choices = - let choices_compare (_,e1,_,_,m1) (_,e2,_,_,m2) = - let m1 = Lazy.force m1 in - let m2 = Lazy.force m2 in - compare (e1,m1) (e2,m2) in - let choices_compare_by_passes (p1,_,_,_,_) (p2,_,_,_,_) = compare p1 p2 in + let choices_compare (o1,_) (o2,_) = compare o1 o2 in + let choices_compare_by_passes (p1,_,_,_) (p2,_,_,_) = + compare p1 p2 in let rec uniq = function [] -> [] | h::[] -> [h] - | (p1,e1,_,_,_)::(p2,e2,d2,o2,m2)::tl when e1 = e2 -> - uniq ((p1@p2,e2,d2,o2,m2) :: tl) + | (o1,res1)::(o2,res2)::tl when o1 = o2 -> + let merge_by_name errors = + let merge_by_env errors = + let choices_compare_by_env (_,e1,_) (_,e2,_) = compare e1 e2 in + let choices_compare_by_passes (p1,_,_) (p2,_,_) = + compare p1 p2 in + let rec uniq_by_env = + function + [] -> [] + | h::[] -> [h] + | (p1,e1,_)::(p2,e2,d2)::tl when e1 = e2 -> + uniq_by_env ((p1@p2,e2,d2) :: tl) + | h1::tl -> h1 :: uniq_by_env tl + in + List.sort choices_compare_by_passes + (uniq_by_env (List.stable_sort choices_compare_by_env errors)) + in + let choices_compare_by_msg (_,_,m1,_) (_,_,m2,_) = + compare (Lazy.force m1) (Lazy.force m2) in + let rec uniq_by_msg = + function + [] -> [] + | h::[] -> [h] + | (p1,i1,m1,s1)::(p2,i2,m2,s2)::tl + when Lazy.force m1 = Lazy.force m2 && s1 = s2 -> + uniq_by_msg ((p1@p2,merge_by_env (i1@i2),m2,s2) :: tl) + | h1::tl -> h1 :: uniq_by_msg tl + in + List.sort choices_compare_by_msg + (uniq_by_msg (List.stable_sort choices_compare_by_msg errors)) + in + let res = merge_by_name (res1@res2) in + uniq ((o1,res) :: tl) | h1::tl -> h1 :: uniq tl in - List.sort choices_compare_by_passes - (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 - | [_,env,diff,loffset,msg] -> - notify_exn - (GrafiteDisambiguator.DisambiguationError - (offset,[[env,diff,loffset,msg]])); + | [loffset,[_,envs_and_diffs,msg,significant]] -> + let _,env,diff = List.hd envs_and_diffs in + notify_exn + (GrafiteDisambiguator.DisambiguationError + (offset,[[env,diff,loffset,msg,significant]])); | _::_ -> let dialog = new disambiguationErrors () in dialog#check_widgets (); @@ -217,30 +361,72 @@ let rec interactive_error_interp ?(all_passes=false) source_buffer notify_exn let model = new interpErrorModel dialog#treeview choices in dialog#disambiguationErrors#set_title "Disambiguation error"; dialog#disambiguationErrorsLabel#set_label - "Click on an interpretation to see the corresponding error message:"; - ignore (dialog#treeview#connect#cursor_changed (fun _ -> - let tree_path = - match fst (dialog#treeview#get_cursor ()) with - None -> assert false - | Some tp -> tp in - let idx = model#get_interp_no tree_path in - let _,env,diff,loffset,msg = List.nth choices idx in - let script = MatitaScript.current () in - let error_tag = script#error_tag in - source_buffer#remove_tag error_tag - ~start:source_buffer#start_iter - ~stop:source_buffer#end_iter; - notify_exn - (GrafiteDisambiguator.DisambiguationError - (offset,[[env,diff,loffset,msg]])) - )); + "Click on an error to see the corresponding message:"; + ignore (dialog#treeview#connect#cursor_changed + (fun _ -> + let tree_path = + match fst (dialog#treeview#get_cursor ()) with + None -> assert false + | Some tp -> tp in + let idx1,idx2,idx3 = model#get_interp_no tree_path in + let loffset,lll = List.nth choices idx1 in + let _,envs_and_diffs,msg,significant = + match idx2 with + Some idx2 -> List.nth lll idx2 + | None -> + [],[],lazy "Multiple error messages. Please select one.",true + in + let _,env,diff = + match idx3 with + Some idx3 -> List.nth envs_and_diffs idx3 + | None -> [],[],[] (* dymmy value, used *) in + let script = MatitaScript.current () in + let error_tag = script#error_tag in + source_buffer#remove_tag error_tag + ~start:source_buffer#start_iter + ~stop:source_buffer#end_iter; + notify_exn + (GrafiteDisambiguator.DisambiguationError + (offset,[[env,diff,loffset,msg,significant]])) + )); let return _ = dialog#disambiguationErrors#destroy (); GMain.Main.quit () in let fail _ = return () in - ignore (dialog#disambiguationErrors#event#connect#delete (fun _ -> true)); - connect_button dialog#disambiguationErrorsOkButton (fun _ -> return ()); + ignore(dialog#disambiguationErrors#event#connect#delete (fun _ -> true)); + connect_button dialog#disambiguationErrorsOkButton + (fun _ -> + let tree_path = + match fst (dialog#treeview#get_cursor ()) with + None -> assert false + | Some tp -> tp in + let idx1,idx2,idx3 = model#get_interp_no tree_path in + let diff = + match idx2,idx3 with + Some idx2, Some idx3 -> + let _,lll = List.nth choices idx1 in + let _,envs_and_diffs,_,_ = List.nth lll idx2 in + let _,_,diff = List.nth envs_and_diffs idx3 in + diff + | _,_ -> assert false + in + let newtxt = + String.concat "\n" + ("" :: + List.map + (fun k,value -> + DisambiguatePp.pp_environment + (DisambiguateTypes.Environment.add k value + DisambiguateTypes.Environment.empty)) + diff) ^ "\n" + in + source_buffer#insert + ~iter: + (source_buffer#get_iter_at_mark + (`NAME "beginning_of_statement")) newtxt ; + return () + ); connect_button dialog#disambiguationErrorsMoreErrors (fun _ -> return () ; interactive_error_interp ~all_passes:true source_buffer notify_exn offset @@ -587,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 @@ -699,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 @@ -778,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 _ = @@ -788,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)); @@ -808,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; @@ -817,12 +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 ~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 := @@ -967,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 *) @@ -1509,18 +1728,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 @@ -1528,12 +1745,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 @@ -1548,19 +1767,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